Code Contracts by Example

So how does one get his feet wet with Design-by-Contract? I remember when I first started using Microsoft Code Contracts I immediately made a huge mess of my projects from which it took several weeks to fully recover. After a while I figured out what worked and what didn't and I've developed a habitual way of doing things that seems to work okay. I won't go so far as to say they are best practices, but they keep me out of trouble. So without delving too deep into the theory of DbC, here are a few of the patterns I use.

Constructor-based Dependency Injection

While property-based DI is possible with code contracts, it gets ugly really quickly. The only way I've been able to make it work is with a backing field and explicit null checks in the getter. Basically, if you have a public setter then all bets are off as far as invariants are concerned. Constructor-based injection, on the other hand, is very clean and straightforward, and allows you to offload some of the work onto the caller. Further, the static checker can leverage readonly fields to infer pre- and postconditions.

public class Foo
{
    private readonly IBar _bar;
    private readonly IBaz _baz;

    public Foo(IBar bar, IBaz baz)
    {
        Contract.Requires(bar != null);
        Contract.Requires(baz != null);
        
        Contract.Ensures(_bar != null);
        Contract.Ensures(_baz != null);

        _bar = bar;
        _baz = baz;
    } 

    [ContractInvariantMethod]
    private void Invariant()
    {
        Contract.Invariant(_bar = bar);
        Contract.Invariant(_baz = baz);
    }
}

The invariants are probably not absolutely necessary, but I've found that the combination of explicit postconditions in the constructor, combined with explicit invariants, speeds up the static analysis and generally has better results.

Conversion of One Nullable Type to Another

I use this frequently for mapping DTOs to domain objects and vice-versa. The contract literally states that either the method parameter is null or the return value will not be null. Put another way, it guarantees that the return value will not be null so long as the method parameter is not null.

public DomainType ToValueObject(DtoType dto)
{
    Contract.Ensures(dto == null || Contract.Result<DomainType>() != null);
    if (dto == null)
    {
        return null;
    }
    return new DomainType(...);
}

Value Objects

When I first started migrating from if/throw blocks I had a lot of preconditions that looked like this:

Contract.Requires(str != null);
Contract.Requires(!string.IsNullOrWhiteSpace(str));
Contract.Requires(Regex.IsMatch(str, @"^[a-zA-Z0-9]+$");
Contract.Requires(str.Length() >= 3);
Contract.Requires(str.Length() < 255);

And so on. Moreover, I found that I had a lot of methods sprinkled about with identical sets of preconditions--usually there was some value that wasn't central to my domain (a telephone number or domain name) that had certain validation requirements in the 3 or 4 places it was used. After performing this conversion I discovered a number of things:

• The responsibility for validation shifted out of my method and onto the caller
• There were far more call sites than methods being called, which meant that these preconditions now had to be checked in many more places than before
• The static checker had to prove the preconditions were met at every call site
• The maintenance burden had increased by an order of magnitude

This was obviously not a move in the right direction. However, all of these issues were resolved by replacing string typed arguments with value objects (not necessarily value types) that had the following characteristics:

• Explicit verification in the constructor
• Postconditions on the constructor ensuring the validity of the newly instantiated instance
• Immutability

The result was that all of the explicit checks moved to one place (the value object constructor) and all instances of the value object type are guaranteed to be always be valid (else the constructor would throw).

I found it helpful to put the validation logic into a public static IsValid method so that callers have a means to defensively validate input without catching exceptions. The result is something like this:

public class ValueObject
{
    private readonly string _value;

    public ValueObject(string str)
    {
        Contract.Ensures(!string.IsNullOrWhiteSpace(_string));
        Contract.Ensures(_string.Length >= 5);
        Contract.Ensures(_string.Length <= 15);
        if (!IsValid(str))
        {
            throw new ArgumentException();
        }
        _string = str;
    }

    public static bool IsValid(string str)
    {
        Contract.Ensures(Contract.Result<bool>() == false || !string.IsNullOrWhiteSpace(str));
        Contract.Ensures(Contract.Result<bool>() == false || str.Length >= 5);
        Contract.Ensures(Contract.Result<bool>() == false || str.Length <= 15);

        if (string.IsNullOrWhiteSpace(str)) return false;
        if (str.Length < 5) return false;
        if (str.Length > 15) return false;
        return true;
    }

    [ContractInvariantMethod]
    private void Invariant()
    {
        Contract.Invariant(!string.IsNullOrWhiteSpace(_string));
        Contract.Invariant(_string.Length >= 5);
        Contract.Invariant(_string.Length <= 15);
    }
}

The contracts for the method calls then could be reduced to simple Contract.Requires(arg != null) checks, which are much easier to prove. This also works well with numeric types such as prices, quantities, percentages, and other such range-restricted values.

Conclusion

DbC requires a lot of investment up front, but it does offer a lot of value. The trick is enforcing contracts that add value and letting other things go. For example, a telephone number may need to be validated against a regular expression, but it usually isn't necessary to express that as a postcondition, especially if none of the callers depend on that fact. Often it's enough to use an if/throw block and leave it at that. In fact, that last point bears repeating: contracts are not a wholesale replacement for if/throw blocks, and are actually inferior in many cases.

It should also be said that DbC alone is no substitute for good design and good programming. If a method has a laundry list of contracts, then it might be that there are simply too many parameters, or too many dependencies between parameters. Sometimes splitting a method into multiple methods with different parameters, or encapsulating a set of parameters into a new type of object will completely obviate the need for complex preconditions. Convoluted preconditions are probably an indication that a method is in need of refactoring, which is valuable in and of itself.

Bottom line, the point of DbC is to formally specify things that both the caller and the callee should be responsible for, so contracts should be limited to things that should have been obvious or inferred to begin with (such as null checks). There are many conditions that are not the responsibility of the caller and should continue to be handled during runtime within the method (such as business logic and complex validation requirements). Done right, DbC will simply help you prove what you already assumed in the first place and identify places in your code where the assumptions are met.