I downloaded code contracts from here. After installing code contract, I tried to create my first project with code contracts. I created new console project name CodeContractTest . I added reference to Microsoft.Contracts library which is appeared in .Net references after installation.

I wrote following code this is clearly compiled without any warning.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
using System.Diagnostics;

namespace CodeContractTest
{
    class Program
    {
        static void Main(string[] args)
        {
            Swap(new string[] { "Code", "Contract" }, 1, 4);
        }
        static void Swap(string[] arr, int item1, int item2)
        {
            string temp;
            temp = arr[item1];
            arr[item1] = arr[item2];
            arr[item2] = temp;
        }

    }

}

However, after running this application we will encounter with IndexOutOfRangeException. This is occurred because illegal parameter in Swap method call.

Let take a look at new feature added to Visual Studio 2008. I open properties window of project. New tab is added named "Code Contracts". I checked "Perform Static Contract Checking" and "Implicit Array Bound Obligations". If I rebuild project new warnings and message will be appeared in Error window.

Four warnings are about Array access and four suggestion message plus one summary message.

In order to improve code and get rid of warnings I should add preconditions in swap method. I added four line of precondition which assure item1 , item2 is in array boundary. I used Contract class and Requires static method which is used for preconditions it has two overloads first overload has a bool parameter. We can use this method to explicitly define the conditions of input parameters.

        static void Swap(string[] arr, int item1, int item2)
        {
            Contract.Requires(item1 < arr.Length);
            Contract.Requires(item1 >= 0);
            Contract.Requires(item2 < arr.Length);
            Contract.Requires(item2 >= 0);
            string temp;
            temp = arr[item1];
            arr[item1] = arr[item2];
            arr[item2] = temp;
        }

After rebuilding project new warning is appeared. It shows that one of contract precondition rules is broken.

If I change the swap with proper input parameters after rebuilding project warning messages will be disappeared.

            Swap(new string[] { "Code", "Contract" }, 0, 1);

If I check "Implicit Non-Null Obligation" on code contracts tab of property window building application will be face with new warning "contracts: Possible use of a null array 'arr'"

Swap method should be called with non-null array parameter. This is another contract that should be added to preconditions. So I changed Swap method as follow.

       static void Swap(string[] arr, int item1, int item2)
        {
            Contract.Requires(arr != null);
            Contract.Requires(item1 < arr.Length);
            Contract.Requires(item1 >= 0);
            Contract.Requires(item2 < arr.Length);
            Contract.Requires(item2 >= 0);
            string temp;
            temp = arr[item1];
            arr[item1] = arr[item2];
            arr[item2] = temp;
        }

In this case developer of Swap method define contract for input parameters and there is no need to swap caller know all swap code in order to prevent bad parameter calling.

You can download code from here

During developing applications we have always use unwritten rule in programming or if it is written in design documents user should consider them in development. For example if developer wants to call a method which has an integer parameter and this parameter is used as an index of array he should be aware calling that method with negative value or greater than array lenght. Calling method with negative value causes runtime error.

There are lots of contracts that a developer should consider during development. Recently I came across new concept (However it is in research phase) named CodeContracts which is really wonderful. It seems that this concept will be in VS 2010. CodeContracts will organized all written and unwritten rules & contract in development. In order to clarify CodeContract usage imagine following code:

static void Swap(string[] arr, int itemIndex1, int itemIndex2)
{
	string temp;
	temp = arr[itemIndex1];
	arr[itemIndex1] = arr[itemIndex2];
	arr[itemIndex2] = temp;
}

What are possible errors when we want to call Swap method?

• None of itemIndex1 and itemIndex2 could be negative (both should be positive)
• None of itemIndex1 and itemIndex2 could be greater than arr.length
• Array arr should be not null

Before code contracts developer should always consider possible situation and avoid breaking rule. But CodeContracts provides rich methods by which you can add your Code Contracts to your method and after compiling application Contracts checker will warn about breaking rules. Let see how it should be implemented with CodeContracts

static void Swap(string[] arr, int itemIndex1, int itemIndex2)
{
	Contract.Requires(arr != null);
	Contract.Requires(itemIndex1 >= 0);
	Contract.Requires(itemIndex1 < arr.Length);
	Contract.Requires(itemIndex2 >= 0);
	Contract.Requires(itemIndex2 < arr.Length);
 
	string temp;
	temp = arr[itemIndex1];
	arr[itemIndex1] = arr[itemIndex2];
	arr[itemIndex2] = temp;
}

I added five contracts to this method which mean this method needs not null array as first parameter, second and third parameter (itemIndex1, itemIndex2) should be greater or equal to zero and should be less than array length.

In the next post I will show how to implement this with CodeContracts

But now I want to introduce some resources:

• Microsoft Research - Code Contracts home page
• Tutorial Video in channel9
• Contract Checking and Automated Test Generation with Pex