Thursday, April 18, 2013

Impressions of Code Contracts

Embroiled in a few projects right now, but one gave me the chance to explore Microsoft's code contracts a little. I was initially excited about the prospect of contracts when they were first announced, hence my crude API-compatible implementation in Sasa.Contracts which allowed me to prepare my codebases for contracts. I've now had a chance to play with the real thing, so we'll see how it holds up to reality.

Going Above and Beyond

As usual, I decided to push the boundaries and try to prove properties beyond what C# and .NET can do natively via their type systems. One common nuisance on the CLR is that you can't specify a default constructor for value types. While even code contracts can't prevent someone from creating an empty struct value, you can possibly prevent the use of such an empty value:

public struct NonNull<T>
    where T : class
{
    readonly T value;
    public NonNull(T value)
    {
        Contract.Requires(value != null);
        this.value = value;
    }
    public T Value
    {
        get
        {
            Contract.Requires(Value != null);
            return value;
        }
    }
}

We have here a simple class that wraps a nullable reference type. The preconditions specified on the constructor ensure that no NonNull instance can be created with an explicit null value. The only remaining possibility is to create a value via default(NonNull<T>), so contracts haven't bought us much there.

However, check out the precondition on the NonNull.Value property: before you can call the property, you have to ensure the property is itself not null. This ensures that only values of NonNull created via the provided constructor can use any value of NonNull!

Here's the failure that Visual Studio reports when it can't prove that the contracts are statically satisfied:

Code Contract Failure in Visual Studio

Mission accomplished! Through some clever application of preconditions, you can probably ensure all sorts of behavioural properties on objects you couldn't verify before, so this is fertile ground for experimentation and optimization.

No Free Lunch

There's always a downside of course, and in this case it's the long contract check times. Visual Studio has an option to check contracts in the background after a build completes, which helps a little.

Also, there are a few limitations and bugs remaining in the MS's static checker. For instance, according to the docs, invariants declared on structs are supposedly ignored (section 6.6.1), but I discovered this isn't completely true (Microsoft Connect bug reported).

I also found another bug while testing the interface contracts, so caveat emptor!

Still, it's a promising framework and I plan to make use of it where I can to improve the reliability of my code. Sasa v0.9.4 will probably be the last release for .NET 3.5, so subsequent releases will exploit contracts as much as possible. In particular, Sasa.NonNull<T> will finally get a static analysis to ensure that property is respected!

No comments: