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, 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-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.

The main people who worked on this project are:

• Mike Barnett
• Manuel Fahndrich
• Francesco Logozzo
• Wolfram Schulte
• 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.

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

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

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

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

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