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
Refer to the things it expect to do. These are expressed using Contract.Requires()
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.
The following example illustrates how the three main features of contracts are used.
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
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
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
c) Object Invariant
public int EMIPercentage
get; private set;
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.