10 Steps for Implementing Code Contracts Static Analysis

I'm a fan of the Code Contracts from Microsoft Research. Adding them to an existing code base can be an exercise in frustration, though. If you turn on static analysis, it can generate thousands of warnings. I have some tips on how to attack those warnings, based on my experience.

Just like C#, I start counting at zero, and actually this list goes to 11.

 0. Change the settings for contracts.

Perform Static Contract Checking in the Background. Turn on all the check boxes except Baseline. It will be slightly faster if you have SQLExpress installed on your computer. Add .\SQLExpress into the SQL Server field. Set the warning level to low. Set the Contract Reference Assembly to build. Change the Extra Static Checker Options to -maxWarnings 5000.

 1. Reduce the problem.

In the assemblyinfo.cs file, add the following line:

[assembly: ContractVerification(false)]

This causes the static analyzer to ignore all of the warnings. Now go to the most basic class in your project and add ContractVerification(true) to the top of it. You can identify these basic classes because they have no dependencies on the other classes in the project. You may find that adding a Class Diagram to the project helps identify these basic classes.

An example of using ContractVerification on a particular class:

[ContractVerification(true)]
public class Foo
{
}

This will cause the static analyzer to only report warnings for that one class. Fix those warnings, then move the [ContractVerification(true)] to the next class you want to work on.

2. Work from the bottom up.

Work on classes that have no dependencies inside your project. Then after you have those cleaned up, work on the ones that only depend on the ones that you have already cleaned up until the entire assembly is complete. Again, adding a Class Diagram to the project may help finding the next class to work on.

3. For each class, add ContractPublicPropertyName attributes to your property backing fields.

For each field that is used to back a property, add the ContractPublicPropertyName attribute to the field showing what public property accesses the field.

[ContractPublicPropertyName("Count")]
private int count = 0;

public int Count
{
    get
    {
        return this.count;
    }
}

4. Add invariants.

Don't worry about other issues until the invariants are in place. I add an invariant section to the bottom of each class like the code below. (I sort my method names alphabetically and I like mine at the bottom of the code, hence the Zz. You can name the method anything you want, but be consistent throughout the project.)

/// <summary>Object invariant.</summary>
[ContractInvariantMethod]
private void ZzObjectInvariant()
{
    Contract.Invariant(this.count >= 0);
}

For each thing will always be true after the constructor is complete, add a contract to the ZzObjectInvariant method. You want the invariants to be in place first because it makes it so you don't need contracts in each individual method or property.

5. Go through each constructor, method, and property set in the class and add contracts.

For each parameter to the method, add appropriate Contract.Requires<exception>() contracts. For example:

public int Foo(Bar bar, int increment)
{
    Contract.Requires<ArgumentNullException>(bar != null);
    Contract.Requires<ArgumentOutOfRangeException>(increment > 0);

    // more stuff
}

For properties, validate the set clause value.

public int Count
{
    get
    {
        return this.count;
    }

    set
    {
        Contract.Requires<ArgumentOutOfRangeException>(value >= 0);
        this.count = value;
    }
}

If there are two conditions, put them into separate contracts rather than using &&. For example:

public int Count
{
    get
    {
        return this.count;
    }

    set
    {
        // not Contract.Requires<ArgumentOutOfRangeException>(value >= 0 && value <= 100);
        Contract.Requires<ArgumentOutOfRangeException>(value >= 0);
        Contract.Requires<ArgumentOutOfRangeException>(value <= 100);
        this.count = value;
    }
}

If a member overrides an inherited member or implements an interface, you will not be able to add Contract.Requires contracts to the member. First see if you can add the Contract.Requires to the class or interface that you are overriding or implementing. If you can't, then add a Contract.Assumes to the code. Adding Contract.Requires to an interface or abstract class requires creating a class that implements the interface or abstract class and decorating it with the ContractClassFor attribute. See sections 2.8 and 2.9 of the Code Contracts user manual.

Understand that depending on your project contract settings these contracts may not be present at run time. Other warnings may report that you are trying to invoke a method or access a property of a null (the dreaded CA1062). Even though it will be impossible to pass in a null if the contract is in place, the code analysis can't count that the contract will be in the delivered code. You will need to add additional code that acts as if the contract doesn't exist and properly handles the condition. It's redundant and has some expense. I like none of the other options, though.

You can throw an exception. This is similar to the legacy Custom Parameter Validation, except this happens after the Contracts, and isn't actually part of them. There is no Contract.EndContractBlock().

public int Foo(Bar bar, int increment)
{
    Contract.Requires<ArgumentNullException>(bar != null);
    Contract.Requires<ArgumentOutOfRangeException>(increment > 0);

    if (bar == null)
    {
        throw new ArgumentNullException("bar");
    }

    // more stuff
}

You can also return an appropriate value, like this:

public int Foo(Bar bar, int increment)
{
    Contract.Requires<ArgumentNullException>(bar != null);
    Contract.Requires<ArgumentOutOfRangeException>(increment > 0);

    int result = 0;

    if (bar != null)
    {
        // more stuff that assigns result
    }

    return result;
}

In both cases, the contract makes it impossible for bar to be null, yet I handle it anyway as if the contract wasn't there. Some day they may make the coordination between the static analyzer and the compiler such that this isn't necessary. You would then have to have code contracts turned on in the shipping version, which you may not want.

6. Go through the methods and properties and add Contract.Ensure contracts.

Add Contract.Ensure methods for all of the return values of the constructors, methods, and properties. You will need Contract.Result<T>() frequently to examine return values. For example:

public int Foo(Bar bar, int increment)
{
    Contract.Requires<ArgumentNullException>(bar != null);
    Contract.Requires<ArgumentOutOfRangeException>(increment > 0);
    Contract.Ensures(Contract.Result<int>() > 0);

    // more stuff
}

7. Fix Bugs.

Compile the code. The static analyzer will complain about various things, such as calling methods on possibly null values. Fix those. This is really the point of the whole exercise. It will warn you about many subtle things that you might have initially thought impossible, but are actually real edge cases.

When you compile the project, it may make suggestions for Contract.Requires and Contract.Assumes. Do not automatically add these. See if there is an invariant that you can add that would handle this for all members. Also see if the code should be handling whatever the warning is suggesting. For example, if the warning suggests adding a Contract.Requires<ArgumentNullException>(value != null), it may be legitimate to be able to pass in null here, but you are performing a method on the value object. You really need an 'if (value != null)' in the code, not a contract. Determining whether null should be allowed requires intimate knowledge of the code.

8. Judiciously add Contract.Assume() calls.

Static analysis is hard. The analyzer has to figure out what the code is doing without running it. In some cases it can't. This is especially true if you use a library that you don't control. Microsoft has been better about adding contracts to the .NET framework, but there is not 100% support yet. For example, using the .NET Framework 4.0, I have this code:

PathGeometry pathGeometry = new PathGeometry();
pathGeometry.Figures.Add(figure);

The static analyzer complains that pathGeometry.Figures might be null. This should never be the case. There is a missing Contract.Ensures in the .NET Framework PathGeometry constructor that .Figures is not null. You can help the analyzer by adding an Contract.Assume() call. Like this:

public int Count
{
    get
    {
        return this.count;
    }

    set
    {
        Contract.Requires<ArgumentOutOfRangeException>(value >= 0);
        this.count = value;
    }
}

The warning about .Figures possibly being null now goes away.

Add Assumes for things that should be impossible in your code.

9. Don't use Contract.Assert.

If the analyzer reports that an Assume can be proven and can be turned into an Assert, just remove the line. The analyzer actually has that knowledge at that point, so you don't need an assert.

10. Don't give up.

When all the warnings are killed, move on to the next class. Move the [ContractVerification(true)] and fix those. When you actually have all the warnings fixed, go back to the assemblyinfo.cs and turn on warnings for the entire assembly and remove the attribute from the individual classes. Then try bumping the warning level up a notch in the project properties and fix some more.

Some of the warnings are a real puzzle as you try to trick the static analyzer to certify your code. Adding more contracts, ensures, and assumes will cause them to go away.