Microsoft Code Contracts

I’m currently working on an ongoing side project, and we’re using Microsoft Code Contracts, so I thought that I would create a series of posts documenting my experience with this as a new and curious user. The basic idea of it is to standardize and formalize preconditions, post conditions, and invariants in your classes.

For instance, let’s say that you work on a C# project in which you can’t really trust your users or your dependencies not to do unpleasant things. You might create a class that looks like this:

public class CarService
{
    private ICarDao _carDao;

    public CarService(ICarDao dao)
    {
        if(dao == null) 
            throw new ArgumentNullException("dao");
        _dao = dao;
    }

    public void SaveCar(Car car)
    {
        if(car == null) 
            throw new ArgumentNullException("car");
        else if(car.Engine == null) 
            throw new InvalidOperationException();
        //etc
        _carDao.Save(car);
    }
...
}

This is the epitome of defensive code, and it’s a smart thing to do in the context that I mentioned. At the beginning of each method, you ferret out the things that will create problems for operations (precondition violations) and throw if they aren’t satisfied. In the constructor, you, perhaps, enforce some class invariants (i.e. our service class basically can’t do anything if its data access reference is null).

That’s fine, but it creates a certain amount of boilerplate overhead, and it’s somewhat ad-hoc. Code Contracts standardizes it:

public class CarService
{
    private ICarDao _carDao;

    public CarService(ICarDao dao)
    {
        Contract.Requires(dao != null);
        _dao = dao;
    }

    public SaveCar(Car car)
    {
        Contract.Requires(car != null);
        Contract.Requires(car.Engine != null);
        //etc
        _carDao.Save(car);
    }
...
}

As you can see, the defensive coding boilerplate becomes a little less verbose. But what’s more is that Code Contracts will also generate compiler warnings when client code does not or may not satisfy the preconditions. So, if I had the code below in another class, I would be shown a compiler warning that the precondition was not satisfied.

public void DoSomething()
{
    CarService myService = new CarService(new CarDao());
    myService.SaveCar(null);
}

Another cool facet of this is that you can express post conditions in a way that you really can’t with the guard/throw paradigm. For instance:

public class Foo
{
    private int _counter;

    public void Increment()
    {
        Contract.Ensures(Contract.OldValue(_counter) + 1 == _counter);
        _counter++;
    }    
}

As you can see, we’re sticking a post condition in here that advertises what the method will guarantee when it is finished. In this fashion, client code that may specify its own pre-/post-conditions and invariants has more to work with in terms of proving its own conditions. Also, anyone reading the code can tell what the author intended the method to do (and what side-effects, if any, it might have). This is where your contract doubles as correctness enforcement and documentation. Comments may lie after enough time and changes, but the contracts won’t–you’ll get warnings or runtime errors if that documentation goes out of date.

The final thing that I’ll show in this introductory post is the notion of a class invariant. Let’s take a look at our previous car example, but dressed up a little.

public class CarService
{
    private ICarDao _carDao;

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(_carDao != null);
    }

    public CarService(ICarDao dao)
    {
        Contract.Requires(dao != null);
        Contract.Ensures(_dao != null);
        _dao = dao;
    }

    public SaveCar(Car car)
    {
        Contract.Requires(car != null);
        Contract.Requires(car.Engine != null);
        //etc
        _carDao.Save(car);
    }
...
}

Here, I’ve added a method decorated with a Code Contracts attribute. The end effect of this is to create an object invariant – essentially, an implied pre- and post-condition for every method in my class. Now, the code is future-proof. If anyone adds methods to this and tries to set _carDao to null, they will get warnings/errors, depending on the mode of Code Contracts. (I’ll go into this in a future post.) If someone derives from this class and tries the same thing, the same result will occur. We’ve locked up an invariant as bulletproof. The other nice thing is that if you move this logic into an invariant method, you don’t have to check the _carDao for null in all of your methods, cluttering them with useless checks.

In future posts, I intend to cover the different modes of Code Contracts, some more advanced features, some more depth information, its interaction with the Pex utility, and a utility that I’m working on which provides wrappers for C# library classes that enforce the No-Throw guarantee.