Code contracts provide a way to specify conditions in your code. For example this may be pre-conditions and post-conditions of methods. These contracts will allow you to validate the parameters of methods and to check the method results.

 
Example application

Within this article I want to use an example application to show the different features of code contracts. The example console application contains a Person class with Name and Age properties. Furthermore the class contains an Initialize method to set up all properties. The following source code shows a basic version of this console application.

class Program
{
    static void Main(string[] args)
    {
        Person myPerson = new Person();

        myPerson.Initialize("John Doe", 28);

        Console.ReadKey();
    }
}

public class Person
{
    private string _name;
    private int _age;

    public string Name { get { return _name; } }
    public int Age { get { return _age; } }

    public void Initialize(string name, int age)
    {
        _name = name;
        _age = age;
    }
}

 
As you can see the properties will be set within the Initialize method by using the method parameters. The actual implementation allows us to define a person with a negative age and a null value as name. Therefore we want to extend the implementation of this method and add some parameter validations. So we define that a name of a person should not be null and the age must be non-negative.

 
If-then-throw pattern

A classic way to implement the parameter validation would be the If-then-throw pattern. By using this pattern the validation will be done in if-statements and in case of not allowed parameters an exception will be thrown. The following source code shows an according extension of the Initialize method.

public class Person
{
    private string _name;
    private int _age;

    public string Name { get { return _name; } }
    public int Age { get { return _age; } }

    public void Initialize(string name, int age)
    {
        // check arguments
        if (name == null)
        {
            throw new ArgumentNullException("name");
        }

        if (age < 0)
        {
            throw new ArgumentOutOfRangeException("age");
        }

        // init properties
        _name = name;
        _age = age;
    }
}

 
Code Contracts

In the previous example you can see a common practice in software development. Any input parameter of the method is checked against the expectations and an exception is thrown if it does not match. With code contracts you may lift up this best practice to the next level. Pre-condition contracts allow you to write such parameter checks in a compact, easy to read and easy to understand way. Moreover code contracts will allow you to clearly state what’s required instead of testing against what isn’t desirable.

Code Contracts, however, aren’t limited to pre-conditions. You may also write post-conditions and invariants. Invariants describe the expected state for an object instance. So they are some kind of post-conditions which are applied to every public method.

 
Preparation

At first you have to install “Code Contracts for .NET”. After installation you will find a new “code contracts” tab within you solution properties. Within this tab you have to activate the option “Perform Runtime Contract Checking”. If these checks are enabled the code contracts will be executed, otherwise the contracts stay in your code but they are not checked and therefore you may execute a method with a not allowed parameter.

 
Pre-conditions

Now we want to modify our example application and use code contracts instead of the if-then-throw pattern. Therefore the two parameter checks will be replaced by two code contracts. The following source code shows the origin version of the method and the modified version with code contracts.

If-then-throw pattern

public void Initialize(string name, int age)
{
    // check arguments
    if (name == null)
    {
        throw new ArgumentNullException("name");
    }

    if (age < 0)
    {
        throw new ArgumentOutOfRangeException("age");
    }

    // init properties
    _name = name;
    _age = age;
}

 
Code contracts

public void Initialize(string name, int age)
{
    Contract.Requires(name != null);
    Contract.Requires(age >= 0);

    //init properties
    _name = name;
    _age = age;
}

 
As you can see, the parameter checks have been switched from an exception approach where checks against the wrong values are performed to a definition of allowed values. For example instead of checking if the age is less than zero we now say we expect a value which is zero or larger. Therefore we now have a real contract for the method. We define all expectations and do not longer try to find all other situations where these expectations are not fulfilled.

 
Post-conditions

Of course, a normal behavior of a method is to use the input parameters, do something and create output parameters or modify the internal state of an object instance. Therefore you always have an expected method result or an expected object instance state when a method terminates.

In our example method the internal properties will be set by the Initialize method. Therefore we have an expected internal state and may write two according post-conditions. The following source code shows the new method with the already implemented pre-conditions and the new post-conditions.

public void Initialize(string name, int age)
{
    Contract.Requires(name != null);
    Contract.Requires(age >= 0);
    Contract.Ensures(Name == name);
    Contract.Ensures(Age == age);

    //init properties
    _name = name;
    _age = age;
}

 
Exceptional post-conditions

If a method throws an exception, the internal state of the object instance may be different compared to the normal execution of the method. Such exception states may be defined by exceptional post-conditions. You can specify these post-conditions by using the Contract.EnsuresOnThrow method.

 
ContractException

Now we have seen pre-conditions and post-conditions. But one major question is not answered at the moment: What happens if a code contract is not fulfilled?

The answer is very easy: A ContractException will be thrown. This is a special exception type which you cannot catch. I will come back to this topic a little bit later and explain why this exception type is used and how you can map the ContractException with other exceptions that you can catch.

 
Invariants

Invariants describe the expected state for an object. So, the object instance must always have this expected state. This will be checked on every public method call. Invariants are not checked for object finalizers and are not called by the Dispose method.

In the example application we have defined that every person must have a non-negative age and a name which is not null. These conditions must be valid for the person instance and therefore for each public method call. So these conditions are perfect candidates for an invariant code contract.

To create an invariant you have to define a private void method which is marked with the ContractInvariantMethod attribute. Within this method you can us Contract.Invariant to specify the invariant contracts. The following source code shows the adapted version of the person class.

public class Person
{
    private string _name;
    private int _age;

    public string Name { get { return _name; } }
    public int Age { get { return _age; } }

    public Person()
    {
        _name = "";
        _age = 0;
    }

    public void Initialize(string name, int age)
    {
        Contract.Requires(name != null);
        Contract.Requires(age >= 0);
        Contract.Ensures(Name == name);
        Contract.Ensures(Age == age);

        //init properties
        _name = name;
        _age = age;
    }

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(Name != null);
        Contract.Invariant(Age >= 0);
    }
}

In the above class I have added property initializations to the constructor. This will set the object instance in a valid state. Without this initialization you cannot create a new object instance because after creation of the instance the invariant code contract will be checked and fails.

 
Performance

According to the functionality of code contracts you may think they are based on reflection. But if you look behind the scene you will see that code contracts do not use reflection. They are realized by using a binary rewriter. This tool modifies the runtime code and injects the contracts. Therefore code contracts have a very good performance.

 
Catch contract exceptions

As mentioned before, code contract exceptions will be thrown as ContractException. This is a private exception of type System.Diagnostics.Contracts.__ContractsRuntime.ContractException which is embedded into your assembly and you cannot catch such an exception.

At first, this sounds like a limitation, but on the other hand contracts and assertions are conditions that must always be true. If they are violated the program can be in a state where it cannot continue safely.

In some special cases you may want create pre-conditions which the calling instance should be catch and do a specific error handling. In such a cases you can map a pre-condition to another exception class by using the command Contract.Requires<Exception>(). Within the demo application we could map the pre-conditions for example to specific argument exceptions. The following source code shows an according adaption of the initialize method.

public void Initialize(string name, int age)
{
    Contract.Requires<ArgumentNullException>(name != null);
    Contract.Requires<ArgumentOutOfRangeException>(age >= 0);
    Contract.Ensures(Name == name);
    Contract.Ensures(Age == age);

    //init properties
    _name = name;
    _age = age;
}

 
Summary

The combination of pre-conditions, post-conditions and invariants will allow you to write more robust applications. Furthermore such code contracts will make the source code more self-explaining and easier to read and understand. The proper use of code contracts will therefore result in higher-quality code.