Code contracts (Part 1): Introduction

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