BT

New Early adopter or innovator? InfoQ has been working on some new features for you. Learn more

Details on Using Code Contracts

| by Abel Avram on Feb 26, 2009. Estimated reading time: 2 minutes |

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.

Rate this Article

Adoption Stage
Style

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

Login to InfoQ to interact with what matters most to you.


Recover your password...

Follow

Follow your favorite topics and editors

Quick overview of most important highlights in the industry and on the site.

Like

More signal, less noise

Build your own feed by choosing topics you want to read about and editors you want to hear from.

Notifications

Stay up-to-date

Set up your notifications and dont miss out on content that matters to you

BT