Microsoft Code Contracts

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 code contracts

• Improved testing: Code contracts provide static contract verification, runtime checking, and documentation generation.

• Automatic testing tools: You can use code contracts to generate more meaningful unit tests by filtering out meaningless test arguments that do not satisfy preconditions.

• Static verification: The static checker can decide whether there are any contract violations without running the program. It checks for implicit contracts, such as null dereferences and array bounds, and explicit contracts.

• Reference documentation: The documentation generator augments existing XML documentation files with contract information. There are also style sheets that can be used with Sandcastle so that the generated documentation pages have contract sections.

Why to use Code Contracts?

Object-oriented languages already include contracts; “classic” signature-checking involves verification of parameter counts and type-conformance. Design-by-contract (DBC) generally means extending this mechanism to include assertions on a higher semantic level. A method’s signature describes the obligations calling code must fulfill in order to execute the method. The degree of enforcement varies from language to language. Statically-typed languages verify types according to conformance at compile-time, whereas dynamically-typed languages do so at run-time. Even the level of conformance-checking differs from language to language, with statically-typed languages requiring hierarchical conformance via ancestors and dynamically-typed languages verifying signatures via duck-typing.

And that’s only for individual methods; methods are typically collected into classes that also have a semantic meaning. DBC is about being able to specify the semantics of a class (e.g. can property A ever be false when property B is true?) as well as those of method parameters (can parameter a ever be null?) using the same programming language.