Overview

Code Contracts bring the advantages of design-by-contract programming to all .NET programming languages. The benefits of writing contracts are:

Improved testability

• each contract acts as an oracle, giving a test run a pass/fail indication.
• automatic testing tools, such as Pex (opens in new tab), can take advantage of contracts to generate more meaningful unit tests by filtering out meaningless test arguments that don’t satisfy the pre-conditions.

Static verification We have prototyped numerous static verification tools over the past years. Our current tool takes advantage of contracts to reduce false positives and produce more meaningful errors.

API documentation Our API documentation often lacks useful information. The same contracts used for runtime testing and static verification can also be used to generate better API documentation, such as which parameters need to be non-null, etc.

Our solution consists of using a set of static library methods for writing preconditions, postconditions, and object invariants as well as three tools:ccrewrite, for generating runtime checking from the contracts

• cccheck, a static checker that verifies contracts at compile-time.
• ccdoc,  a tool that adds contracts to the XML documentation files and to Sandcastle (opens in new tab)-generated MSDN-style help files.

The use of a library has the advantage that all .NET languages can immediately take advantage of contracts. There is no need to write a special parser or compiler. Furthermore, the respective language compilers naturally check the contracts for well-formedness (type checking and name resolution) and produce a compiled form of the contracts as MSIL. Authoring contracts in Visual Studio allows programmers to take advantage of the standard intellisense provided by the language services. Previous approaches based on .NET attributes fall far short as they neither provide an expressive enough medium, nor can they take advantage of compile-time checks.

• Contracts are expressed using static method calls at method entries. Tools take care to interpret these declarative contracts in the right places. These methods are found in the System.Diagnostics.Contracts namespace.
• Contract.Requires takes a boolean condition and expresses a precondition of the method. A precondition must be true on entry to the method. It is the caller’s responsibility to make sure the pre-condition is met.
• Contract.Ensures takes a boolean condition and expresses a postcondition of the method. A postcondition must be true at all normal exit points of the method. It is the implementation’s responsibility that the postcondition is met.

Full details are in the user documentation (opens in new tab).

The main people who worked on this project are:

• Mike Barnett (opens in new tab)
• Manuel Fahndrich
• Francesco Logozzo
• Wolfram Schulte (opens in new tab)
• Herman Venter

There were also many others, especially interns:

• Mehdi Bouaziz
• Scott Carr
• Patrick and Radhia Cousot
• Diego Garbervetsky
• Jacque-Henri Jourdan
• Vincent Laviron
• Mathias Peron
• Daryl Zuniga

Our tools can be installed in any Visual Studio edition (except Express). The license does allow commercial use. It is available on the Visual Studio Gallery (opens in new tab).

After installing please use the link to the documentation under All Programs -> Microsoft Code Contracts to get you started.

(opens in new tab)If your project uses Code Contracts and would like to have it added to this list, please let us know! Code Contracts is available with a commercial license on the Visual Studio Gallery (opens in new tab)

• Autodiff (opens in new tab)
• Boogie (opens in new tab)
• CCI (opens in new tab)
• Centricity Enterprise Archive (opens in new tab)(Commercial medical DICOMXDS archive)
• Connected Properties (opens in new tab)
• Dafny (opens in new tab)
• Facebook C# SDK (opens in new tab)
• DbExecutor (opens in new tab)
• Elysium (opens in new tab)
• FT Toolkit (opens in new tab)
• Labs Framework (opens in new tab)
• Mishra Reader (opens in new tab)
• NColony (opens in new tab)
• Nito AsyncEx (opens in new tab)
• QuickGraph (opens in new tab)
• Extensions for Reactive Extensions (opens in new tab)
• ResX Resource Manager (opens in new tab)
• Sando (opens in new tab)
• Shweet (opens in new tab)
• Scrabble for WPF (opens in new tab)

• Channel 9 Videos (opens in new tab)
• Visual Studio 2010 Editor Extensions (opens in new tab) (21 September 2010)
• Pex and Code Contracts (opens in new tab) on their Danish tour! (21 May 2010)
• Getting Started with Code Contracts (opens in new tab) (23 February 2009)
• Code Contracts Documentation (opens in new tab) (10 August 2009)
• Code Contracts Static Checker (opens in new tab) (22 December 2009) Also available in Italian (opens in new tab)!
• Code Contracts and Pex (opens in new tab) (23 April 2009) Also available in French (opens in new tab)!
• PDC2008 Presentation (opens in new tab)
• PDC2009 Presentation (17 November 2009)
• Francesco Logozzo introduces the Code Contracts API (opens in new tab) to Italian programmers (in Italian).

• Sputnik coding gets started with CodeContracts, Nov 2011
• A five part series by Dino Esposito (opens in new tab) in the Cutting Edge column from MSDN Magazine (opens in new tab):
  • Give Your Classes a Software Contract (opens in new tab), April 2011
  • Code Contract Settings in Visual Studio 2010 (opens in new tab), May 2011
  • Invariants and Inheritance in Code Contracts (opens in new tab), June 2011
  • Inheritance and the Liskov Prinicple (opens in new tab), July 2011
  • Static Code Analysis and Code Contracts (opens in new tab), August 2011
• Kevin Hazzard (opens in new tab) does a multiple part introduction. Now up to Chapter 8 (opens in new tab)!
• Jasper shows how contracts work for abstract types and interfaces (opens in new tab)— June 6, 2010
• Derik Whittaker looks at how to use Assert, Assume, ForAll, and Exists (opens in new tab)— May 31, 2010
• Jasper takes a look at object-invariants (opens in new tab) — May 30, 2010
• Gunnar Peipman shows how to validate arrays and collections (opens in new tab)with CodeContracts — May 28, 2010
• Exoteric uses CodeContracts in modelling die rolls (opens in new tab)— May 28, 2010
• Jasper (opens in new tab)examines postconditions — May 27, 2010
• Gunnar Peipman looks at how the compiled contracts look after rewriting (opens in new tab) — May 22, 2010
• Jasper (opens in new tab)looks a preconditions in more detail — May 20, 2010
• Jasper (opens in new tab)is starting a series on CodeContracts — May 17, 2010
• Fernando Machado Píriz (opens in new tab)shows off the beneficial interaction of CodeContracts and PeX — May 8, 2010
• Gunnar Peipman (opens in new tab) shows examples of CodeContracts and testing — May 6, 2010
• YOOT (opens in new tab) uses contracts in an implementation of Value Objects — March 22, 2010
• xosfaere (opens in new tab)ponders implication operators — March 15, 2010
• Jeffrey Richter talks about Code Contracts at DevWeek Conference (opens in new tab)— March 16, 2010
• Jordan .NET User Group (opens in new tab)covers Code Contracts — Feb 25, 2010
• xosfaere (opens in new tab)provides an introduction — Feb 28, 2010
• Doug Finke showcases the static checker (opens in new tab) — Feb 27, 2010
• Developer days in Scottland has a session (opens in new tab)on CodeContracts — Feb 27, 2010
• Matthias Jauernig compares Design-by-contract and Test-driven-development (opens in new tab)part 4 — Feb 14, 2010
• Roy Dictus discusses CodeContracts by Example (opens in new tab) — Feb 3, 2010
• Matthias Jauernig compares Design-by-contract and Test-driven-development (opens in new tab)part 3 — Feb 6, 2010
• Rober McCarter talks about suppressing warnings (opens in new tab) when using CodeContracts — Feb 5, 2010
• rantings in the dark gets inspired and creates jsContract (opens in new tab), i.e., CodeContracts for Javascript — Feb 3, 2010
• Matthias Jauernig compares Design-by-contract and Test-driven-development (opens in new tab)part 2 — Jan 30, 2010
• Matthias Jauernig compares Design-by-contract and Test-driven-development (opens in new tab)part 1 — Jan 23, 2010
• Martin Lapierre’s article (opens in new tab)on CodeContracts and Pex — Jan, 2010
• DaveT provides an overview of CodeContracts (opens in new tab) — Jan 12, 2010
• Francesco Logozzo talks about the static checker on Channel 9 (opens in new tab) — Dec 22, 2009
• Peli and MaF talk about CodeContracts in French (opens in new tab) — Dec 17, 2009
• Blog entry on CodeContracts and NUnit (opens in new tab)— Dec 13, 2009
• Dino Esposito talks about asserts and assumes (opens in new tab) — Nov 11, 2009
• Relentless Development blog ponders the future with CodeContracts (opens in new tab) — Nov 11, 2009
• Vaideeswaran covers postconditions and invariants (opens in new tab) — Nov 3, 2009
• Vaideeswaran covers preconditions and postconditions (opens in new tab) — Oct 29, 2009
• Dino Esposito introduces invariants (opens in new tab) — Oct 21, 2009
• Eric Swanson has a slide deck on Code Contracts (opens in new tab) — Oct 13, 2009
• Dino Esposito introduces postconditions (opens in new tab) — Oct 2, 2009
• Sankarsan blogs about CodeContracts (opens in new tab)— Sep 27, 2009
• Matthias Jauernig talks about the documentation feature of CodeContracts (opens in new tab)— Sep 13, 2009
• Dino Esposito introduces preconditions (opens in new tab) — Sep 9, 2009
• Jani Järvinen writes an introduction to Code Contracts (opens in new tab) — Sep 4, 2009
• Jomit blogs about Code Contracts (opens in new tab)— Sep 1, 2009
• Matt describes how contracts are written on interfaces (opens in new tab)— Aug 28, 2009
• Matt describes object invariants (opens in new tab)— Aug 27, 2009
• Matt describes postconditions (opens in new tab)— Aug 26, 2009
• winSharp talks about interface contracts (opens in new tab) — Aug 16, 2009
• winSharp talks object invariants (opens in new tab)— Aug 7, 2009
• karthick discusses validation using CodeContracts (opens in new tab)— Jul 25, 2009
• winSharp provides an overview of CodeContracts (opens in new tab) — Jul 19, 2009
• Stefano Ricciardi discusses Contracts and inheritance (opens in new tab) — Jul 17, 2009
• winSharp discusses pro and cons of parameter validation with CodeContracts (opens in new tab) — Jul 13, 2009
• Derik Whittaker posts a video on CodeContracts (opens in new tab) — Jul 2, 2009
• Derik Whittaker discusses object invariants (opens in new tab) — Jul 1, 2009
• Stefano Ricciardi introduces CodeContracts (opens in new tab)— Jun 26, 2009
• Mary Jo Foley (opens in new tab) — March 2, 2009
• TechRepublic (opens in new tab) — March 2, 2009
• eWeek (opens in new tab) — February 24, 2009
• Soma’s Blog (opens in new tab) — February 24, 2009
• InfoWorld (opens in new tab) — February 24, 2009