Introduction to Microsoft Code Contracts with Visual Studio 2008

Design by Contract was first introduced by Bertrand Meyer, creator of the Eiffel programming language,  in his seminal book Object-oriented Software Construction. In a nutshell, DBC is based on the following principles:

• preconditions: a method imposes on the client a set of conditions that must be met in order for the method to be invoked successfully (think about parameters validation).
• postconditions: a set of properties are guaranteed by the method immediately after the execution (think about a return value that can only be positive, for example).
• invariants: a set of properties on the class are assumed to hold before the method starts and are guaranteed to hold after the method completes (think about a field of the class that may not be negative, for example).

A contract formalizes these three things. How can contracts, and defensive programming in general, help us developing better software? Bertrand Meyer explains it in this interview from 2003:

The main purpose of contracts is to help us build better software by organizing the communication between software elements through specifying, as precisely as possible, the mutual obligations and benefits that are involved in those communications. [...] relying on these notions—that is to say, making sure when you write software that don't just write the implementation, but also write the more abstract properties underlying the implementation in the form of contracts—provides a greatly added software development experience in several respects. It helps ensure correctness in the first place, helps debugging, helps testing, helps ensure inheritance is properly handled, helps managers, provides a quite effective form of documentation, and a few others.

Up to now, only a few languages supported DBC natively, and C# was not one of those. With .NET 4.0 Microsoft fills this gap with Code Contracts. It's possible to download Code Contracts for Visual Studio 2008 for the Standard Edition and the Team System edition.

A Basic Example

Let's see a basic example of how one can use Contracts in a simple class. (to try this on your own you need to install Code Contracts from msdn web site). In this case I have a class with a static method that simply inverts the content of a string (the choice of the algorithm here is irrelevant).

using System;
using System.Diagnostics.Contracts;
namespace TestContracts
{
  public class StringInverter
  {
    public static string Invert(string s)
    {
      // preconditions:
      Contract.Requires(s != null);
      // postconditions;
      Contract.Ensures(Contract.Result<string>().Length == s.Length);
      char[] reverted = new char[s.Length];
      int i = 0;
      foreach (char c in s)
      {
        reverted[s.Length - 1 - i ] = c;
        i++;
      }
      
      return new string(reverted);
    }
  }
}

The first thing to notice is that we have added a reference to the System.Diagnostics.Contracts namespace. This is where the new library is located. For this to work you have also to add a reference in your project to the Microsoft.Contracts assembly that has come with the Code Contracts installation.

The first method that we invoke on Contracts is a precondition that specifies that this method cannot accept an input string which is null (it would accept an empty string though). The second method is a postcondition asserting that this method guarantees that the string returned by this method will have the same size as the input string.

Obviously you are free to add more preconditions and/or postconditions if your domain logic requires so. But what exactly happens at run-time if either a precontion or a postcondition is not met? The answer is: it depends. After installing Code Contracts, project properties displays a new tab at the bottom named "Code Contracts" where you can tweak the contracts behavior for each of the build configurations that you have defined (Debug, Release, etc...).

Let's concentrate on Runtime Checking for now: after you have checked it, you can decide which kind of contracts to enable; you should refer to official documentation for a complete explanation of all the options. For now, let's just pick "Full" and check "Assert on contract failures". With this choice, pre and postconditions will be tested at runtime and if any of them is not met a dialog will be shown detailing the failing condition.

So, let's try calling the Invert method with a null string and let's see what happens. Add the following code to the class above, compile and run.

public static void Main()
{
  Console.WriteLine(Invert(null));
}

This is what you should see:

As you can see, this looks exactly like using Debug.Assert calls from System.Diagnostics (many of us, myself included, used debug asserts in place of preconditions). In reality, contracts are much more powerful since

• you can not just enforce preconditions but also guarantee postconditions and other class invariants
• contracts knows about class hierarchies: you can define contracts on interfaces and base classes and they will be inherited from derived classes
• it's possible to analyse compliance to contracts in a static way, even without running the code!

We'll discuss about all this in the next post. Stay tuned!

Next post in the series: Code Contracts: Invariants.