.NET Code Contracts Tutorial

Code Contracts are new in .NET 4, they come from the Microsoft Labs Spec# program.

What are .NET Code Contracts?

Code Contracts give you a way to put your assumptions into the code, so they are documented and available to anyone who uses your code. The assumptions can alert another developer when a method is being called incorrectly, similiar to putting a try catch block and throwing your own exceptions.

Installing .NET Code Contracts

Even if you have .NET 4 and Visual Studio 2010 you will still need to do an install to get all the features.

There are two versions of Code Contracts, you will need to install one of these:

Code Contracts Standard Edition
This version installs if you have any edition of Visual Studio other than the Express Edition. It includes the stand-alone contract library, the binary rewriter (for runtime checking), the reference assembly generator, and a set of reference assemblies for the .NET Framework.

Code Contracts Premium Edition
This version installs only if you have one of the following: Visual Studio 2008 Team System, Visual Studio 2010 Premium Edition, or Visual Studio 2010 Ultimate Edition. It includes the static checker in addition to all of the features in the Code Contracts Standard Edition.

Setup Code Contracts

Once you have installed Code Contracts, create a new Console Application and right-click on your project in Visual Studio’s Solution Explorer and click Properties.
There should be a new tab at the bottom called Code Contracts. It will look similiar to this (I’m showing the standard version in this example):
code contracts

Thats all you need and your ready to go.

Code Contract Examples

Here is a simple example of using Contract.Requires:

using System.Diagnostics.Contracts;

private static void Main(string[] args)

public static void DoRequires(string input)
    Contract.Requires(input != null);

If you run that code you will get an exception window appear in Visual Studio you will get a contract exception pop up with the following message “Precondition failed: input != null”.

Using the Requires method lets you check Preconditions, to ensure that everything is the way you want before your method starts doing it’s work.

Here’s another example:

private static void Main(string[] args)
    DoRequiresForAll(new List<string>() {"test",null,"blah"});

public static void DoRequiresForAll(List<string> input)
    Contract.Requires(Contract.ForAll(input, w => w != null));

This uses the Contract.ForAll method to ensure that no value in the array is null.

There is also an Assert similiar to Debug.Assert:

Contract.Assert(input > 0);

You can use Asserts to test any condition you like, not just preconditions.

There is also a way to test postconditions.

public static int DoEnsures()
    Contract.Ensures(Contract.Result<int>() > 0);
    return 0;

This example ensures that the return value is greater than zero, by using the Contract.Result generic.

You can also use contracts on methods that pass data using the “out” parameter:

public static void DoEnsuresWithOut(out int inputOutput)
    Contract.Ensures(Contract.ValueAtReturn(out inputOutput) == 10);
    inputOutput = 5;

The Contract.ValueAtReturn checks the value of the parameter passed to it before it is returned.

More About .NET Code Contracts

By using Code Contracts you can quickly document your assumptions and conditions of your code, all with a nice framework that lets you control the level of conditions to use.

Check out the Documentation for Code Contracts.

I would also recommend taking a look at the Microsoft Labs page for Code Contracts.

Categories:   Code