Code Contracts in .NET 4

Overview

One of the new features that’s included in .NET 4 is something called Code Contracts. (In fact Code Contracts are available already, but they're being made a standard part of the Framework in .NET 4.)

I'll say up front that I haven't really used Code Contracts yet, but I like the basic idea so thought it'd be worth writing down a quick summary of what they do.

Code contracts allow you to specify various conditions, or contracts, that must be met by your code and / or any code that calls it.  These contracts can be enforced with a combination of static (reported by the tools) and run time checking (reported by asserts or exceptions).

There are three types of contracts:

• Preconditions – these specify conditions that function arguments must satisfy when a function is called.
• Postconditions – these specify conditions about the return value, or the state of the object when a function returns.
• Object Invariants – these specify conditions that the public state of the object always meets.

The main aim of Code Contracts is to formalise coding assumptions you make, and to help find and locate bugs in your code.  The Code Contracts are written in code so that they are human readable, and so that they can be analysed and enforced by the tool chain.

An Example

Examples always help, so here we go:

Preconditions:

// Calling this function with null, or with an object with TestValue less than zero 
// would fail the contract
public static void MyTestContractFunction(MyTestContractClass testItem)
{
  // Preconditions:
// Ensures testItem is null. 
// Throw NullReferenceException if not satisfied at run-time
Contract.Requires<NullReferenceException>(testItem != null); // Always compiled in
Contract.Requires(testItem.TestValue >= 0); // Compiled in depending on tool options

}

Or an alternative, more familiar way:

public static void MyTestContractFunction(MyTestContractClass testItem)
{
  // You can also write code contracts in the 'old-style' argnull exception way
  if ( testItem == null )
    throw new NullReferenceException("test item must not be null");

  // But you need to specify the end of the contracts
// i.e. if statements up to here classed as contracts
  Contract.EndContractBlock();

  // Do stuff...
}

Postconditions:

public static void MyOtherFunction(MyTestContractClass testItem)
{
  // Do stuff...

  // This line would cause the post-condition to fail
// (if it compiled- there appears to be a bug in the tools?!?)
  //testItem.TestValue = 0;

  // Postconditions:
  Contract.Ensures(testItem.TestValue >= 0); 
} 

Getting Started

To get started you need to download the tools as although the libraries are included in .NET 4, the tools aren’t.

The tool chain uses binary re-writing to enable runtime checking, as well as generating xml documentation to include contracts and performing static checking of code to catch potential violations at compile time (Visual Studio Team System version only).

Check out the following links to get more detail about Code Contracts and how they work:

CLR Inside Out: Code Contracts

Code Contracts FAQ

Getting Started With Code Contracts Video (VS2008)