BT

Details on Using Code Contracts

by Abel Avram on Feb 26, 2009 |

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:

contracts

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

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Tell us what you think

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread
Community comments

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Email me replies to any of my messages in this thread

Discuss

Educational Content

General Feedback
Bugs
Advertising
Editorial
InfoQ.com and all content copyright © 2006-2014 C4Media Inc. InfoQ.com hosted at Contegix, the best ISP we've ever worked with.
Privacy policy
BT