Home > .NET, Custom Development > Code Contracts in dot NET

Code Contracts in dot NET

Kevin Code Contracts

June 24th | 2010

Code Contracts in dot NET

It is often desirable for a developer, particularly those who make public APIs, to communicate to 3rd party developers what their code expects. For example, say I have a product that allows plugins to be written for it. A plugin can call an API I provided, “Print”. Print takes a single string, however, the string should never be null.
Nonetheless, we can’t guarantee a developer will never pass in null; there may be a bug in their application. To prevent serious errors from occurring, we need to ensure our parameter is never null. We can do this with an exception.

public void Print(string data)
{
    if (data == null)
        throw new ArgumentNullException("data",
"This parameter must not be null.");
    //Implementation omitted
}

This is a very typical pattern but it leaves us wanting more. The developer won’t know he is giving the API a string that cannot be used until he attempts to run the application. Nothing is stopping the compiler from compiling.
Statically checking if our code is violating a contract is a powerful feature. An experimental language called Spec# currently supports this but unfortunately, being experimental, it makes it difficult to use in real-world scenarios.
Enter Code Contracts. Now built into the .NET Framework 4, all you need to do is download an add-on for Visual Studio 2008 or 2010. In the .NET Framework 4, the magic happens in the System.Diagnostics.Contracts namespace. You can download the add-on from here:
http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx
Once installed, you will see a new tab on your project’s properties called “Code Contracts”.

I’ve configured a few key options here. I’ve set the “Perform Runtime Contract Checking” to Full, and checked the “Perform Static Contract Checking”, “Check in Background”, and “Show squigglies”. Next, we need to define the contracts. We can use the Contract class to indicate these contracts. Our method now looks like this:

public static void Print(string data)
{
    Contract.Requires<ArgumentNullException>(data != null);
    //Implementation omitted
}

This will have the same behavior as before: If data is null, then an ArgumentNullException is thrown. However, in addition to the runtime failure, we will also see a warning when we compile and squigglies under the code.

And of course, if we set “r” to something not null, the contract is happy! However, what happens if r is getting data from somewhere else?

static void Main(string[] args)
{
    string r = SomeMethodThatWillNeverReturnNull();
    Print(r);
}

private static string SomeMethodThatWillNeverReturnNull()
{
    return "notnullstring";
}

The contract analyzer isn’t small enough to check and see what the method actually does. However, the method could potentially return null. We know better than that, so we can tell the Code Contract analyzer that the return value is never null. This is done with a post condition using Contract.Ensure. A post condition is a contract that ensures a condition is met when the method is exiting. In our case, we want a post condition that says “SomeMethodThatWillNeverReturnNull” won’t return null.

private static string SomeMethodThatWillNeverReturnNull()
{
    Contract.Ensures(Contract.Result<string>() != null);
    return "notnullstring";
}

This tells us that the result of the method will never return null. The call to Print is now satisfied knowing that its source of data cannot return null. If SomeMethodThatWillNeverReturnNull could return null, then the post condition will fail.
Let’s go over what we are seeing. The Contract.Requires indicates that the Print method requires its data parameter as not null, before the method is actually executed. If the condition fails, an exception is raised at runtime, and a warning is generated at compile time.
Contract.Ensures is a post condition. It indicates that before the method exits, that condition must be met. Though it is a post condition, it’s still recommended that the constraint be placed at the top of the method. Let’s say we need our code to meet this contract:

  1. Print must never accept a null string.
  2. Print must never accept a string that is greater than 1000 characters.
  3. When print is called, we must set dataWasPrinted to true.

Here is what our contract looks like:

class Program
{
    private static bool dataWasPrinted = false;

    static void Main(string[] args)
    {
        string data = GetData();
        Print(data);
    }

    private static string GetData()
    {
        Contract.Ensures(Contract.Result<string>() != null);
        Contract.Ensures(Contract.Result<string>().Length <= 1000);
        return "data from file";
    }

    public static void Print(string data)
    {
        Contract.Requires<ArgumentNullException>(data != null);
        Contract.Requires<ArgumentNullException>(data.Length <= 1000);
        Contract.Ensures(dataWasPrinted == true);
        try
        {
            //Implementation omitted
        }
        finally
        {
            dataWasPrinted = true;
        }
    }
}

This is a powerful concept and can be extremely useful. I wouldn’t recommend putting contract validation on all of your code, rather just public methods that will be exposed to others. I might also recommend using it in critical cases where a specific contract must be met. It isn’t a replacement for unit tests or mock testing, rather another tool in the belt that makes a software developer’s life easy.

Kevin Jones is a Team Lead at Thycotic Software, an agile software services and product development company based in Washington DC. Secret Server is our flagship password management software product. On Twitter? Follow Kevin

Categories: .NET, Custom Development
  1. No comments yet.
  1. No trackbacks yet.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: