C# Corner

Code Contracts in .NET 4

Patrick Steele looks into C# Code Contracts under .NET 4 and how they can streamline code validation.

• By Patrick Steele
• 06/22/2010

One of the key features of the .NET Framework is its enforcement of strong typing. But sometimes, simply enforcing that an integer is passed into a method isn't enough. We have to write additional code to make sure the integer is in a particular range or some other requirement. With Code Contracts, we get a language-neutral way to express such additional requirements in the form of preconditions, postconditions and invariants.

What is Code Contracts
Code Contracts is a subset of a larger Microsoft Research Project called Spec# (pronounced "Spec Sharp"). You can read more about this project here. Spec# is a formal language for defining API contracts. A subset of these contracts -- preconditions, postconditions and invariants -- has made its way into Visual Studio 2010 in the form of Code Contracts.

Before being able to utilize Code Contracts, you'll need to download and install it from http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx. Why the need for the download? Code Contracts has support for both Visual Studio 2008 as well as 2010. Since it's not a VS 2010-specific product, a separate download is required.

Parameter Validation
We've all written code to validate parameters sent in to our methods:

public void Withdraw(Account account, decimal amount)
{
	if( account == null)
	{
		throw new ArgumentNullException("account", "account cannot be null");
	}
	if( amount <= 0 )
	{
		throw new ArgumentException("amount must be greater than zero", "amount");
	}
	...
}

This type of validation code is always at the top of our methods and runs before the method does its real work. The work can only continue if these conditions are met (i.e. the account is not null and the amount to withdraw is greater than zero). These are called preconditions and we can use Code Contracts to make these sorts of checks a bit clearer.

The above parameter validation code can be rewritten with Code Contracts as:

public void Withdraw(Account account, decimal amount)
{
	Contract.Requires(account != null, "account cannot be null");
	Contract.Requires(amount > 0, "amount must be greater than zero");
	...

}

The method call to "Contract.Requires" is used to set up preconditions that must be valid for code execution to continue. How does this translate into parameter validation? If you look at the properties for a project after Code Contracts has been installed, you'll notice a new property page called, ironically, "Code Contracts" (Figure 1).

[Click on image for larger view.]

Figure 1. Code Contracts Property Page.

Notice that there is a Configuration dropdown. You can set up your Contract validations specific to each configuration. This allows you to pick and choose when the contracts are validated -- only Debug, both Debug and Release or whatever combination you choose.

If you check "Perform Runtime Contract Checking," Visual Studio will execute an extra step after compiling your application. It invokes the Code Contracts rewriter. This rewriter will examine the compiled IL for usage of the Contract methods and "re-write" the IL with calls to ensure your contracts are followed.

If a null "account" value is passed in to the Withdraw method, a ContractException will be thrown:

[Click on image for larger view.]

Figure 2. ContractException.

Post Conditions
Code Contracts also has the ability to perform post conditions. These are conditions to be checked just prior to exiting a method.

Let's say we're calculating a discount based on some code. This discount amount will be subtracted from the customer's total due. Obviously, we'd never want a negative discount as this would increase the amount the customer owes -- not really a discount! Sure, we can write unit tests for this, but with Code Contracts we can enforce it.

Without code contracts, we'd have to store the computed discount in a variable and make sure our code always exits at a specific location -- which is where we'd validate the discount amount to be non-negative. With Code Contracts, it's much easier. Here's an example that compiles just fine, but will actually fail at runtime:

public double CalculateDiscount(int originalAmount, string discountCode)
{
	Contract.Ensures(Contract.Result<double>() >= 0);

	return -32;
}

The first line of the method sets up a postcondition that the result (i.e. return value) of this method must be greater than zero. How can code at the beginning of a method be used to check what is being returned at the end of the method? That's where the rewriter comes in. It will actually rearrange the original, compiled IL code so that the value returned from the method is stored in a local variable. A common exit point in the method will then execute all of the contract postconditions. It's all the code we'd normally have to write ourselves.

This is just a brief sample of what Code Contracts can do. If you're interested in knowing more, let me know and I can revisit the topic in more detail.