Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation.
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 plan is to add further tools. For instance, we have an internal prototype for a VS 2010 add-in so that inherited contracts show up as you type.
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.
Download
There are two distinct downloads: an academic license download that anyone can play with for non-commercial use (e.g. teaching), and a commercial use download:
Academic License: For any Visual Studio 2008 edition (except Express). Allows non-commercial use. Download link.
Commercial License: There are two commercial versions. See the DevLabs information for more details.
After installing either version, there is link to documentation under All Programs -> Microsoft Code Contracts to get you started.
Contact us
Please use our new msdn forum for contract releated discussions, questions, bug reports, and suggestions.
You can also email us codconfb _at_ microsoft _dot_ com .
Project Members
- Melitta Andersen
- Mike Barnett
- Manuel Fähndrich
- Brian Grunkemeyer
- Katy King
- Francesco Logozzo
- Vipul Patel
- Daryl Zuniga
Current version: 1.2.30312.0
(12 Mar 2010)
- Download (Academic License)
- Release Notes
- Frequently Asked Questions
- User manual
- Papers and documentation
Videos
- Channel 9 Videos
- Getting Started with Code Contracts (23 February 2009)
- Code Contracts Documentation (10 August 2009)
- Code Contracts Static Checker (22 December 2009)
- Code Contracts and Pex (23 April 2009) Also available in French!
- PDC2008 Presentation
- PDC2009 Presentation (17 November 2009)
Now on DevLabs!
Code Contracts is now available with a commerical use license on DevLabs!! Download it now!
There are two versions:
- Team System Edition (includes the static checker)
- Standard Edition (everything except for the static checker)
See what others are saying about us
- Mary Jo Foley -- March 2, 2009
- TechRepublic -- March 2, 2009
- eWeek -- February 24, 2009
- Soma's Blog -- February 24, 2009
- InfoWorld -- February 24, 2009
