Details on Using Code Contracts

InfoQ informed on the availability of Code Contracts for .NET. This time we want to offer more details on using Code Contracts, an important addition to .NET.

Before .NET 4.0, Contracts are added to a Visual Studio project by referencing the library Microsoft.Contracts.dll that is installed under %PROGRAMFILES%/Microsoft/Contracts/PublicAssemblies. .NET 4.0 will contain Contracts in mscorlib.dll. Contract validation can be specified to be executed statically at build time or dynamically at runtime. There are several types of contracts: Preconditions, Postconditions, Object Invariants, Assertions, Assumptions, Quantifiers, Interface Contracts, Abstract Method Contracts.

Preconditions are defined using Contract.Requires() and the result of its compilation appears in IL if the symbol CONTRACTS_FULL or CONTRACTS_PRECONDITIONS is used. An example is:

Contract.Requires( x ! = null );

This precondition is generally used for parameter validation when entering a method’s body as in the example below:

public Rational( int numerator, int denominator) {
   Contract.Requires( denominator ! = 0 );
   this .numerator = numerator;
   this .denominator = denominator;
}

If the condition specified by Contract.Requires() is not met, then Debug.Assert(false) is called followed by Environment.FailFast(). When a precondition is wanted to be present in the assembly, no matter what symbols are used during compilation, then Contract.RequiresAlways() should be used.

Postconditions are contracts to be met when a methods ends, and are specified with Contract.Ensures() as in the next example:

public int Denominator {
  get {
     Contract.Ensures( Contract.Result<int>() != 0 );
     return this .denominator;
  }
}

While the condition is specified before return, it is actually executed after the return value is computed but before the execution is handed to the caller.

Object Invariants are conditions specified for each instances of a class.

[ContractInvariantMethod]
protected void ObjectInvariant () {
   Contract. Invariant ( this .denominator ! = 0 );
}

Other types of contracts are assertions, Contract. Assert(), and assumptions, Contract.Assume(). A failing Assers() will call Debug.Assert(false). Assumptions are similar to assertions at runtime, but differ during static verification. Assumptions are used to specify conditions that are supposed to be met but which the compiler cannot verify due to its limitations.

Interface Contracts are used to specify conditions for interfaces. They are specified using separate classes associated to the interfaces because an interface method declaration cannot have a body. The same is true for abstract methods contracts.

An example of a class using contracts is:

Useful links: InfoQ news on Code Contracts, Code Contracts Download (MSI), Code Contracts online documentation (PDF), Microsoft Research Code Contracts website.