Code Contracts in Visual Studio 2010

Visual Studio 2010 has support for code contracts that allow to express pre-, post-conditions and invariants to your .NET code.

Let’ say you want to create a function to return a random value in a range. This could look like it:

    class Program
    {
        Random rng = new Random();

        public int GetRandom(int min, int max)
        {
            return rng.Next(min, max);
        }

        static void Main(string[] args)
        {
            Program p = new Program();
            int n1 = p.GetRandom(10, 20);
            int n2 = p.GetRandom(10, 10);
        }
    }

However, at a rough analysis one can find two problems:

Second call to GetRandom(), is not well formed, because the range is 0
Radnom.Next returns a value greater or equal to the first argument, and lower than the second.

What code contracts provide is a mean to check that some statements, like:

maximum value of the range should always be greater than the minimum value
returned value should always be in the interval, equal or greater than the minimum, and equal or less than then maximum

The first is a pre-requisite, and the second is a post-requisite. We can specify those with:

        public int GetRandom(int min, int max)
        {
            Contract.Requires(max > min);
            Contract.Ensures(Contract.Result() >= min && 
                             Contract.Result() <= max);

            return rng.Next(min, max);
        }

The Contract class is available in namespace System.Diagnostics.Contracts. To enable the static checking, you have to go to Project Properties > Code Contracts and select “Perform Static Contract Checking.”

When you build, you get the following warnings:

The first says that the call GetRandom(10, 10) does not match the pre-condition. The second warning indicates that the post-condition is not met. It isn’t possible to know whether Random.Next() returns a value that hods the post-condition. But if you check the “Perform Runtime Contract Checking” it asserts at runtime, when the return value is outside the interval (not possible with this code sample).

You can read more about code contracts on the BCL team’s blog. It features a list of possible constructs for pre- and post-requisites, but also object invariants.

Code Contracts are also available for Visual Studio 2008. For downloads and additional information check the following links: