Code Contracts in Visual Studio 2010

Visual Studio 2010 has support for code contracts that allow to express pre-, post-conditions and invariants to your .NET code.

Let’ say you want to create a function to return a random value in a range. This could look like it:

However, at a rough analysis one can find two problems:

  • Second call to GetRandom(), is not well formed, because the range is 0
  • Radnom.Next returns a value greater or equal to the first argument, and lower than the second.

What code contracts provide is a mean to check that some statements, like:

  • maximum value of the range should always be greater than the minimum value
  • returned value should always be in the interval, equal or greater than the minimum, and equal or less than then maximum

The first is a pre-requisite, and the second is a post-requisite. We can specify those with:

The Contract class is available in namespace System.Diagnostics.Contracts. To enable the static checking, you have to go to Project Properties > Code Contracts and select “Perform Static Contract Checking.”

Code Contracts Property Page
Code Contracts Property Page

When you build, you get the following warnings:

Code Contracts warnings
Code Contracts warnings

The first says that the call GetRandom(10, 10) does not match the pre-condition. The second warning indicates that the post-condition is not met. It isn’t possible to know whether Random.Next() returns a value that hods the post-condition. But if you check the “Perform Runtime Contract Checking” it asserts at runtime, when the return value is outside the interval (not possible with this code sample).

You can read more about code contracts on the BCL team’s blog. It features a list of possible constructs for pre- and post-requisites, but also object invariants.

Code Contracts are also available for Visual Studio 2008. For downloads and additional information check the following links:

1 Reply to “Code Contracts in Visual Studio 2010”

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.