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 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
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.
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
- Mike Barnett
- Sheldon Blauman
- Manuel Fähndrich
- Brian Grunkemeyer
- Immo Landwerth
- Francesco Logozzo
- Daryl Zuniga
- Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Francesco Logozzo, Automatic Inference of Necessary Preconditions, in in Proceedings of the 14th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'13), Springer Verlag, January 2013
- Mehdi Bouaziz, Francesco Logozzo, and Manuel Fahndrich, Inference of Necessary Field Conditions with Abstract Interpretation , in 10th Asian Symposium on Programming Languages and Systems (APLAS 2012), Springer, December 2012
- Patrick Cousot, Radhia Cousot, Francesco Logozzo, and Mike Barnett, An Abstract Interpretation Framework for Refactoring with Application to Extract Methods with Contracts, in Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12), ACM SIGPLAN, 23 October 2012
- Francesco Logozzo and Tom Ball, Modular and Verified Automatic Program Repair, in Proceedings of the 27th ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA'12), ACM SIGPLAN, 23 October 2012
- Francesco Logozzo, Patrick Cousot, Radhia Cousot, Manuel Fahndrich, and Mike Barnett, A Semantic Integrated Development Environment, in Companion of the Proceedings of the to the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2012), ACM SIGPLAN, October 2012
- Manuel Fahndrich, Michael Barnett, Daan Leijen, and Francesco Logozzo, Integrating a Set of Contract Checking Tools into Visual Studio, in Proceedings of the 2012 Second International Workshop on Developing Tools as Plug-ins (TOPI 2012), IEEE, 3 June 2012
- Francesco Logozzo, Our Experience with the CodeContracts Static Checker, in Proceedings of the Verified Software: Theories, Tools, and Experiments, Springer, January 2012
- Manuel Fahndrich and Francesco Logozzo, Checking Compatibility of Bit Sizes in Floating Point Comparison Operations, in Proceedings of the 3rd workshop on Numerical and Symbolic Abstract Domains, Electronic Proceedings in Theoretical Computer Science, September 2011
- Francesco Logozzo, Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk, in Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), Springer Verlag, January 2011
- Patrick Cousot, Radhia Cousot, and Francesco Logozzo, Contract Precondition Inference from Intermittent Assertions on Collections, in Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'11), Springer Verlag, January 2011
- Patrick Cousot, Radhia Cousot, and Francesco Logozzo, A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis, in Proceedings of the 38th Symposium on Programming Languages (POPL'11), Association for Computing Machinery, Inc., January 2011
- Manuel Fahndrich and Francesco Logozzo, Static contract checking with Abstract Interpretation, in Proceedings of the Conference on Formal Verification of Object-oriented Software (FoVeOOS 2010) , Springer Verlag, October 2010
- Manuel Fahndrich, Static Verification for Code Contracts, in SAS'10 Proceedings of the 17th international conference on Static analysis , Springer Verlag, September 2010
- Patrick Cousot, Radhia Cousot, and Francesco Logozzo, Contract Precondition Inference from Intermittent Assertions on Collections, no. MSR-TR-2010-117, September 2010
- Mike Barnett, Manuel Fahndrich, and Francesco Logozzo, Embedded Contract Languages, in ACM SAC - OOPS, Association for Computing Machinery, Inc., March 2010
- Vincent Laviron and Francesco Logozzo, Refining Abstract Interpretation-based Static Analyses with Hints, in Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009), Springer Verlag, December 2009
- Michael Barnett, Manuel Fahndrich, Francesco Logozzo, Peli de Halleux, and Nikolai Tillmann, Exploiting the Synergy between Automated-Test-Generation and Programming-by-Contract, in Proc. 31st International Conference on Software Engineering (ICSE'2009) , IEEE, May 2009
- Francesco Logozzo and Vincent Laviron, SubPolyhedra: A (more) scalable approach to infer linear inequalities, in Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'09), Springer Verlag, January 2009
- Francesco Logozzo and Manuel Fahndrich, Pentagons: A Weakly Relational Abstract Domain for the Efficient Validation of Array Accesses, in Science of Computer Programming, Springer Verlag, 2009
- Pietro Ferrara, Francesco Logozzo, and Manuel Fähndrich, Safer unsafe code for .NET, in Proceedings of the 23rd ACM Conference on Object-Oriented Programming (OOPSLA'08), Association for Computing Machinery, Inc., October 2008
- Francesco Logozzo and Manuel Fähndrich, Pentagons: A weakly relational domain for the efficient validation of array accesses, in Proceedings of the 23th ACM Symposium on Applied Computing , Association for Computing Machinery, Inc., March 2008
- Francesco Logozzo and Manuel Fähndrich, On the Relative Completeness of Bytecode Analysis versus Source Code Analysis, in Proceedings of the International Conference on Compiler Construction, Springer Verlag, 2008
- User Forum
- Release Notes
- Frequently Asked Questions
- User manual
- Papers and documentation
- VS 2010 Editor Extensions
- Download
- Documentation
- Watch the video
Projects Using Code Contracts
-
Centricity Enterprise Archive
(Commercial medical DICOM\XDS archive)
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
Videos
- 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).
Who we are
We are a cross-group collaboration made up of people from the RiSE group in MSR and the CLR team.
You've got to check this out!
You can play with Pex and Code Contracts without installing anything on your machine! Just use it from any web browser.
Code Contracts in the News and Blogs
- 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
