Codeharder

The basic idea of programming by contact (or design by contract if you will) is that you can define a contract for an object that will guarantee specified input and output for its callers. Typically this is done with preconditions, postconditions, and invariants.

• Preconditions: a rule that must be true in order for the execution of some code. Think of a precondition as validating that the input is within a specified range.
• Postconditions: a rule that must be true after the execution of some code. A post condition could be ensuring that the object being returned meets a given criteria.
• Class invariants: used to constrain the objects of a class. If you have a queue you may want to constrain it to only contain a certain number of objects.

Spec# is a research project by Microsoft that brings this concept to .net, and shipping with v4 it is referred to Code Contracts. The formal definition is:

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation.

Now that we have an idea of what programming by contract it,what does it look like? Typically how one would go about this was by checking some value, and throwing an exception if it wasn’t valid.  If you were creating an object pool, and wanted to implement a contract it could look something like this.

public class ObjectPool<T> where T : new()
{
    private List<T> pool;
    private int maxItems;
    
    public ObjectPool(int startingCapacity, int maxItems)
    {
        //preconditions that constrain the input.
        if (startingCapacity < 1)
            throw new ArgumentOutOfRangeException("startingCapacity");

        if (maxItems < startingCapacity)
            throw new ArgumentOutOfRangeException("maxItems");
            
        pool = new List<T>(startingCapacity);
        maxItems = maxItems;
    }

    public T GetObject()
    {
        T result = GetNextObject();

        //postcondition: just an example. You proabably wouldn't do this
        if (result == null)
            throw new Exception("The returned object was null");
            
        return result;
    }
    
    private T GetNextObject()
    {
        return default(T); //dummy implementation
    }
    
    private void EnsureCapacity()
    {
        //invariant : just an example, you probably wouldn't do this
        if (pool.Count > maxItems)
        {
            throw new Exception("The returned object was null");
        }
    }
}

It works, but it feels sloppy, and it will only get executed at runtime. Code Contracts actually give you static analysis of the code, and will let you know if you are validating the contract before hand.

public class ObjectPool<T> where T : new()
{
    private List<T> pool;
    private int maxItems;

    public ObjectPool(int startingCapacity, int maxItems)
    {
        //preconditions that constrain the input.
        Contract.Requires(startingCapacity > 0, "startingCapcity must be >0");
        Contract.Requires(maxItems > startingCapacity,"maxItems must be >startingCapcity");

        pool = new List<T>(startingCapacity);
        maxItems = maxItems;
    }

    public T GetObject()
    {
        T result = GetNextObject();

        //postcondition: just an example. You proabably wouldn't do this
        Contract.Ensures(result != null);

        return result;
    }

    private T GetNextObject()
    {
        return default(T); //dummy implementation
    }

    [ContractInvariantMethod]
    private void EnsureCapacity()
    {
        Contract.Invariant(this.pool.Count < this.maxItems);
    }
}

If I were to try to initialize ObjectPool<T> with (0,10) I would see a warning before I even compiled it.

.net programming, code contracts, .net4