Code Contracts - .NET Features

How do you make sure your method guarantees to operate correctly under defined expected input states? Well Code Contracts may help you.

One of the fine features provided by .net 4.0 is Code Contracts. First it’s worth thinking a little about what contract means to you. They indicate the expected input states under which the method guarantees to operate correctly.

Contracts act as checked documentation of your external and internal APIs to be shipped. The code contracts are used to improve testing via runtime-checking, enable static contract verification. One of the interesting features of Code Contracts is that it includes a MSIL rewriter (ccrewrite.exe) that post-processes an assembly to change the intermediate language instructions emitted by the compiler. Another great feature of Code Contracts is that you can turn static analysis on and off on a per project basis. I believe this will be important to anyone practicing TDD and BDD.

A code contract follows design principle of Design By Contract (Dbc). This principle has 3 tenets which code contract also takes care of
a) Pre-condition:
Refer to the things it expect to do. These are expressed using Contract.Requires()

b) Post-condition:
Refer to the things it guarantees to do. These are expressed using Contract.Ensures()

c) Object Invariant:
Refer to things it maintains.

These are expressed using Contract.Invariant() Well, the tenets are fine for Dbc and .Net Code Contract follows each of these properly.
We will examine each of them in this article.

How?
The following example illustrates how the three main features of contracts are used.

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

The preconditions are generally used to specify valid parameter values. The example provided makes sure or checks that the denominator is not equal to zero. We can throw error if the condition is not satisfied using the overloaded method as below.
The example provided makes sure or checks that the denominator is not equal to zero. We can throw error if the condition is not satisfied using the overloaded method as below

b) Post-condition
Contract.Ensures(this.Result!= 0);

Basically the postconditions are checked /Executed before exiting the method call. The example provided checks/ Ensures that the result is not equal to zero. We can throw an exception if the condition is not satisfied using an overloaded method.

Contract.EnsuresOnThrow<ArgumentException> (this.Result!=0);

c) Object Invariant
public int EMIPercentage
{
get; private set;
}

[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(this. EMIPercentage >= 0);
}

The object invariants are conditions that should hold on each instance of your class whenever the object is visible. They express the condition under which the object is in a “good” state. The methods are identified with [ContractInvariantMethod] attribute. The invariants are checked at the end of each public method call. In the example above the denominator will checked at the end of each public method.