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
Subscribe