Better code with C# code contracts


Software developers, aka code monkeys, have a creative profession. Every problem can be solved in a multitude of ways and a developer will apply his knowledge and experience to create what he believes to the best solution. Experience is good, but sometimes not so good. Experience can lead to routine behavior when it comes to writing code and this can mean that you might be tempted to take shortcuts or make assumptions that go unchallenged. A fresh view, for instance by having someone do a code review, may help you, but there may not be time or resources for such a review. Microsoft Code Contracts is a tool that that will help you look at your own code with a different mindset. The goal of code contracts is to improve the predictability of your code. It does this by defining not just contracts, but also by quantifying your assumptions and then performing analysis to warn you when you violate a contract or assumption.
 
What is Microsoft Code Contracts?
Microsoft Code Contracts is an add-on that you can install in Visual Studio (or use via the command line). The add-on offers a number of attributes and helper classes to help formalize any assumptions you make in your code into a contract. A contract can pertain to pre-conditions, post-conditions, assumptions and “object invariants”. The aim of the contract is to document both your internal as well as external APIs and then, as part of compiling the code you can have your code checked to see if you violated a contract.
 
Installation & configuration
Installing the Microsoft Code Contracts package will add an extra configuration tab to your projects in Visual Studio, see figure 1. The main options to enable are runtime and static checking.

 
Figure 1: A new tab with configuration options for Code Contracts.
 
A first look at contracts: pre-conditions
The most primary form a code contract is defining a pre-condition. Take for instance the following method:

public
 double Divide (int number, int divisor)
{
    return number / divisor;
}

The code is functionally correct and after perhaps one or two tests we are satisfied with the implementation. Or are we? We “assume” that the caller of the method will never call “Divide” and pass a zero as the divisor. That would lead to an (unexpected) DivideByZeroException. The following code would be a great improvement, since such a mistake would at least lead to a much better error message:
 
public double Divide( int number, int divisor )
{
    if ( divisor == 0 )
        throw new ArgumentOutOfRangeException(
            "divisor",
            "Divide by zero is not allowed."
            );

 
    return number / divisor;
}
 
By adding defensive code we have defined something that already looks a little like a contract. Throwing an informative exception at runtime is great, but wouldn’t it be better if we warned about a possible mistake at compile time? This is where Microsoft Code Contracts come to the rescue.
 
public double Divide( int number, int divisor )
{
    Contract.Requires( divisor != 0 );
 
    return number / divisor;
}
 
The above code defines, as something that is obviously a contract, that the divisor can never be zero. Should the divisor be zero (at runtime) then a ContractException is thrown. Informative, but not really great, luckily there is an overload on the Requires method that allows specification of a specific exception as well as a custom message:
 
public double Divide( int number, int divisor )
{
    Contract.Requires<ArgumentOutOfRangeException>(
        divisor != 0,
        "Divide by zero is not allowed."
        );
 
    return number / divisor;
}
 
At this point we have defined a contract, with a useful message in case of a violation. At runtime this will show the same behavior as defensive code, but with the added benefit of supporting static checking and thus providing a compiler warning at compile time, more on this later.
 
Runtime checking
The sample in the previous paragraph shows how to define pre-conditions and use the contract to implement runtime checking of these pre-conditions. Enabling runtime checking is done by checking the feature in the Code Contracts tab of your project.
Should you be working on some extremely performance critical code you may opt to enable the runtime checking while doing functional testing and then disable runtime checking when you get ready to do performance testing and deploying your code to production.
 
Static checking
Things get more interesting when looking at checking your code when compiling or even while you’re typing the code. This is called static checking. The code contracts static checker will analyze your code and provide warnings as soon as it detects a violation of a contract.
 
Figure 1 shows that the option “Show squigglies” is enabled. This means that the Code Contract analyzer will highlight my code when it does not meet the requirements laid down in the contract. Figure 2 shows that additional information about the violation can be obtained by hover the mouse over the squigglies.

 
Figure 2: Intellisense squigglies provide direct feedback.
 
Each squiggly is a warning and all warnings are displayed in the Compiler Result window of Visual Studio when you compile the application.
 
NOTE: The “Treat warnings as errors” option currently does not apply to warnings generated by the code contracts analyzer. These warnings will always remain warnings.
 
Post-condition
Where pre-conditions define what to expect from the caller of a function, post-conditions let us define rules about the result of a function.
 
Consider the following code:
 
public int RandomDivisor()
{
    int d = new Random().Next( 100 );
    return d;
}
 
public void Test()
{
    int g = 10;
    int d = RandomDivisor();
 
    var x = Divide( g, d );
}
 
The above code will generate a static checker warning when we call “Divide”. This is correct since we cannot guarantee that the RandomDivisor method won’t return a zero.
 
The following code fixes that problem:
 
public int RandomDivisor()
{
    int d = 0;
    while ( d == 0 )
    {
        d = new Random().Next( 100 );
    }
    return d;
}
 
Great! Now anyone doing a code review can tell that RandomDivisor will never return zero. But... it’s not defined as a contract. With the Contract.Ensures method we add contract rules to define what the result of a method is. Let’s backup a minute and add a contract to the “bad” code:
 
public int RandomDivisor()
{
    Contract.Ensures( Contract.Result<int>() != 0 );
 
    int d = new Random().Next( 100 );
    return d;
}
 
The above code makes a claim about the result of RandomDivisor which is not true and the static checker will generate a warning stating that the ensures is unproven, see figure 3.
 


Figure 3: Unproved contract.
 
If we implement the earlier fix the warning goes away:
 
public int RandomDivisor()
{
    Contract.Ensures( Contract.Result<int>() != 0 );
 
    int d = 0;
    while ( d == 0 )
    {
        d = new Random().Next( 100 );
    }
    return d;
}
 
public void Test()
{
    int g = 10;
    int d = RandomDivisor();
 
    var x = Divide( g, d );
}
 
 
The warning within the Test() method is gone now that we’ve ensured by means of a contract that the RandomDivisor will never return zero.

Assumptions
When writing code we actually do a lot more assumptions than you might think and this is something that will become very clear as soon as you start using code contracts because the static checker will warn you about most of them.
 
Suppose that the RandomDivisor method is implemented by a third party component and makes no Code Contract claims. We can read the documentation and know that they’ve implemented some defensive code. That’s great, but how can we tell the static checker? Contract.Assume offers the option to define assumptions, see code below:
 
 
public void Test()
{
    int n = 10;
    // RandomDivisor is implemented by 3rd party
    int d = RandomDeler();
 
    Contract.Assume( d != 0, "We assume d is never zero." );
 
    return Divide( n, d );
}
 
Not only does the static checker know about our assumption, but a meaningful runtime exception will be thrown if we have runtime checking enabled.

Object Invariants
Pre-conditions and post-conditions are focused on defining contracts on methods. We may also have a need for saying something about the state of an object. It’s hard to come up with a concise example, but let’s assume we have a class “SpecialPoint” where the Y-coordinate is always greater than the X-coordinate:
 
public class SpecialPoint
{
    public int X { get; set; }
    public int Y { get; set; }
 
    public SpecialPoint(int x, int y)
    {
        Contract.Requires<ArgumentException>( y > x );
        X = x;
        Y = y;
    }
}
 
Even though the above code is a step in the right direction, there no guarantuee that at all times Y is greater than X. W could easily write the following code and not break the contract:
 
public void Test()
{
    var p = new SpecialPoint( 10, 20 );
    p.X = 30;
}
 
To write a rule about the state of the object we need to a Contract Invariant Method to the SpecialPoint class. The contract invariant method is a private method which we should never call from our own code, but which the static checker will use to verify the object state. This looks like this:
 
public class SpecialPoint
{
    public int X { get; set; }
    public int Y { get; set; }
 
    public SpecialPoint ( int x, int y )
    {
        Contract.Requires<ArgumentException>( y > x );
        X = x;
        Y = y;
    }
 
    [ContractInvariantMethod]
    private void ClassContract()
    {
        Contract.Invariant( Y > X );
    }
 
}
 
By adding the ClassContract method and adding the ContractInvariantMethod attribute the static checker will now detect a violation when looking at the p.X = 30; statement and generate the appropriate warning.

Contracts and interfaces
An interface is a contract at class level to promise to implement certain functionality. A contract add a level of detail to that initial contract.
 
Suppose we have the following IRandom interface:
 
public interface IRandom
{
    int RandomDivisor();
}
 
Instead of leaving it up to the implementor of IRandom to think about whether to check for returning zero or not we want to add a level of detail to the interface definition.
Code Contracts offers a feature for this via two specific attributes: the ContractClassAttribute and the ContractClassForAttribute. The code below demonstrates how this works:
 
 
[ContractClass( typeof( ContractForIRandom ) )]
public interface IRandom
{
    int RandomDivisor();
}
 
[ContractClassFor( typeof( IRandom ) )]
public abstract class ContractForIRandom : IRandom
{
 
    #region IRandom Members
 
    public int RandomDivisor()
    {
        Contract.Ensures( Contract.Result<int>() != 0 );
        return default( int );
    }
   #endregion
}  
 
public class MyRandomizer : IRandom
{
 
    #region IRandom Members
 
    public int RandomDivisor()
    {
        return 0;
    }
 
    #endregion
}
 
By having the interface refer to a contract class (and strangely the contract class needs to refer back to the interface) the static checker knows that a contract specification applies to any methods that are implemented as part of the interface implementation. The implementation of RandomDivisor() in the MyRandomizer class will generate a warning (and squigglies) to inform the developer that the contract is broken.
 
NOTE: An incomplete implementation of the interface will generate a compiler error and the project will not break. Breaking the contract of the interface will merely generate a warning and your project will still compile.

Always on or off?
Code Contracts are enabled or disabled at project level. You may want to gradually introduce code contracts to an existing project and only check specific classes or methods.
You can enable code contracts at project level and then disable it at assembly level using the following assembly level attribute:
 
[assembly: Contracts.ContractVerification(false)]
 
Subsequently you can enable checking at class or method level by using the same attribute to enable contract verification:
 
[ContractVerification( true )]
public double Divide( int number, int divisor )
{
    Contract.Requires<ArgumentOutOfRangeException>(
        deler != 0,
        "Divide by zero is not allowed."
        );
 
    return number / divisor;
}
 
Closing remarks
Code Contracts allow for an elegant way to perform parameter checking. The code written to add defensive behavior can then be used to perform static checking and generate warnings while writing code and compiling code. A bug caught early is a bug that never happened! When you start using Code Contracts you’ll find yourself looking at your own code with a different set of eyes, essentially doing a code review without needing a separate code reviewer!

Links
· Download Microsoft Code Contracts : http://research.microsoft.com/en-us/projects/contracts/ (short: http://bit.ly/MePem )
 
About the author
Mark Blomsma is an instructor for DevelopMentor, an independent contractor / software architect for Develop-One and a technology advisor for Omnext.NET. He has been awarded the Microsoft MVP Award seven years running for his contributions as a speaker and author for various .NET communities. You can find his blog at http://blog.develop-one.com.