Code Contracts

What is Code Contracts

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation.
For more information visit http://research.microsoft.com/en-us/projects/contracts/

How To use Code Contracts

Code Contracts are designed as a tool to facilitate the software testing and not as part of software logic. In fact when a contract fail, it throw a ContractException and this exception is private. This means that it is impossible (excluding strange hacks) catch the exception and menage it.

Why to use Code Contracts

First of all, using Code Contracts is a good way to develop solid code and to reduce to the minimum the semantic errors.
Contracts could look like the famous asserts but they have several important differences:
  1. The rules can be checked both statically at compile-time and at runtime when the application executes.
  2. Within postconditions, the method's return value can be referred to via the expression Contract.Result<T>(), where T is replaced with the return type of the method.
  3. Within a postcondition, an old expression refers to the value of an expression from the pre-state by using the method Contract.OldValue<T>(e), where T is the type of e.
A further advantage is the automatic generation of Contracts' documentation in XML. Finally this tool could become really useful if flanked by a unit tests generator such as Pex.

Pex

Microsoft Pex is a Visual Studio add-in for testing .NET Framework applications. It automatically generates test suites with high code coverage. It finds interesting input-output values of the methods, which you can save as a small test suite.
Pex generates input values by analyzing the program code. For every statement in the code, Pex eventually tries to create input values that will reach that statement. Pex performs a case analysis for every conditional branch in the code—for example, if statements, assertions, and all operations that can throw exceptions. In other words, the number of input values that Pex generates depends on the number and possible combinations of conditional branches in the code. Pex operates in a feedback loop: it executes the code multiple times and learns about the program's behavior by monitoring the control and data flow.
Pex for fun is a simplified version of Pex that allow you to play with Pex and Code Contracts without installing anything on your machine, just use it from any web browser. An example page is Pex For Fun.

Install Code Contracts and Pex

Requirements:
  • Visual Studio 2010 Installed
Download last version of Code Contracts from http://research.microsoft.com/en-us/projects/contracts/ and install it.
Download last version of Pex from http://research.microsoft.com/en-us/projects/pex/ and install it.

How to use it

Launch Visual Studio and create a new C# Console Project.
In this example we'll implement the binary search in an array. This algorithm has an important precondition: the array must be ordered. Regarding the postconditions we will check that the returned index is between -1 (included) and the size of the array. -1 mean the search haven't found the value.
Copy and paste the code below in the autogenerated main class

public static int binarySearch(int[] a, int val) 
{
    Contract.Requires(isOrdered(a)); //precondition
    Contract.Ensures((Contract.Result<int>() >= -1) && ((Contract.Result<int>() < a.Length))); //postcondition

    int size = a.Length;
    int lower = 0;
    int upper = size;
            
    while (lower <= upper) 
    {
        int i = lower + (upper-lower)/2;
        if (val == a[i]) {
            return i;
        } else if (val < a[i]) {
            upper = i-1;
        } else {
            lower = i+1;
        }
    }
    return -1;
}
where isOrdered(a) is defined as

public static bool isOrdered(int[] a)
{
    bool ordered = true;
    for (int i = 0; i < a.Length - 1; i++)
        if (a[i] > a[i + 1]) ordered = false;
    return ordered;
}
Now, in the main method call binarySearch(int[],int) with different parametres to test it such as the following examples

Console.WriteLine(binarySearch(new int[] { 1, 2, 3, 4 }, 2)); //Ok
Console.WriteLine(binarySearch(new int[] { 2, 3, 4, 5 }, 1)); //Ok
Console.WriteLine(binarySearch(new int[] { 1, 3, 2, 4 }, 3)); //ContractException 
Console.WriteLine(binarySearch(new int[] { 1, 3, 2, 4 }, 8)); //ContractException
Before to build, assure that Code Contract is enabled.
To enable it: Click on project → Menu → Project → <Project-Name> Properties... → Code Contracts → Enable Perform Runtime Contract Checking.

enableContracts.jpg

Build the project and start it. You will note that the third and the fourth test will rise a ContractException due to the precondition becouse the array isn't ordered.
Note that the postconditions are located at the beginning of the method but, actually, they will run when the method return something.

Let's try now to generate further tests with Pex.
First of all, define the class as public otherwise Pex cannot exprole the code and cannot generate the unit tests.
Right-click in the body of the binarySearch method, and click Run Pex.

runPex.jpg

Pex will generate 12 unit tests.

pexGeneratedTests.jpg

In the view we can see 4 failed tests and it means that Pex found some possibly bugs for us!
The failure of test 1 is caused by the instruction

int size = a.Length;
We can simply fix that bug by adding a precondition

Contract.Requires(a != null);
The tests 6 and 12 failed becouse we assigned the size of array to upper variable but, actually, it rappresent the position of last element in the array.
So, let's change

int upper = size;
with

int upper = size-1;
Finally, it's possible to save the output of Pex in real unit tests.
Right-click on generated test → Save Test.. → Apply

pexSaveTests.jpg

Last edited Jul 31, 2011 at 12:08 PM by giuseppe_santoro, version 42