# Saturday, February 28, 2009

image

Ealier this week, we released the Code Contracts library for .NET. Since then, I’ve implemented a lot for contracts for the data structures in QuickGraph . In this post, I’ll talk about my experience with the contracts…

image

Walking through some contracts.

Let’s take a look at the contracts of AddEdge, a method that adds an edge to a graph. Adding an edge to a graph is certainly a fun adventure, when you write contracts for it. Let’s take a look:

public interface IMutableEdgeListGraph<TVertex, TEdge> : ...
    where TEdge : IEdge<TVertex>
{
    /// <summary>
    /// Adds the edge to the graph
    /// </summary>
    /// <param name="edge"></param>
    /// <returns>true if the edge was added, otherwise false.</returns>
    bool AddEdge(TEdge edge);

Interface contracts

Since IMutableEdgeListGraph is an interface, we need to store the contracts in separate class. To do so,  we ‘bind’ the interface and the contract class to each other using the ContractClassForAttribute/ContractClassAttribute.

    [ContractClass(typeof(IMutableEdgeListGraphContract<,>))]
    public interface IMutableEdgeListGraph<TVertex, TEdge> ...
    [ContractClassFor(typeof(IMutableEdgeListGraph<,>))]
    sealed class IMutableEdgeListGraphContract<TVertex, TEdge>
        : IMutableEdgeListGraph<TVertex, TEdge>
        where TEdge : IEdge<TVertex>

Once both types are bound, you can start implementing the contracts of the interface in the contract class. Note that the contract class must use explicit interface implementations for all methods.

Basic null checks

If you care about null references, the first contract will probably to ensure the edge is not null. To make it quick and painless, make sure you use the crn snippet. Note that since the method body of the contracts does not matter, we simply return the default value.

bool IMutableEdgeListGraph<TVertex, TEdge>.AddEdge(TEdge e)
{
    Contract.Requires(e != null);
    return default(bool);
}

More pre-conditions

One of the implicit requirement of AddEdge is that both vertices should already belong to the graph. We want to make this explicit as a pre-condition as well:

bool IMutableEdgeListGraph<TVertex, TEdge>.AddEdge(TEdge e)
{
    IMutableEdgeListGraph<TVertex, TEdge> ithis = this;
    Contract.Requires(e != null);
    Contract.Requires(ithis.ContainsVertex(e.Source));
    Contract.Requires(ithis.ContainsVertex(e.Target));

There are two things to notice here: (1) we had to cast the “this” pointer to the interface we are writing contracts for, IMutableEdgeListGraph<,>. Because the methods in a contract class must be explicit interface implementations, we do not have access to the members of this interface from the “this” pointer, (2) ContainsVertex had to be annotated with [Pure], as any method called from a contract must be pure:

[Pure]
bool ContainsVertex(TVertex vertex);

What about post-conditions

One of my favorite feature of Code Contracts is to be able to state post-conditions. This is done by calling the Contracts.Ensures method. For example, we start by expressing that the edge must belong to the graph when we leave AddEdge:

bool IMutableEdgeListGraph<TVertex, TEdge>.AddEdge(TEdge e)
{
    IMutableEdgeListGraph<TVertex, TEdge> ithis = this;
...
Contract.Ensures(ithis.ContainsEdge(e));

Result and Old

Since the method returns a boolean, we should also state something about the result value. To refer to the result, one has to use the Contract.Result<T>() method. In this case,  the method returns true if the edge was new, false if it was already in the graph. We can refer to a pre-state, i.e. the value of this.Contains(e) at the beginning of the method***:

Contract.Ensures(Contract.Result<bool>() 
== Contract.OldValue(!ithis.ContainsEdge(e)));

Lastly, we can also make sure the edge count has been incremented, if an edge was actually added (as you can see, we could use an implication operator in C#):

Contract.Ensures(ithis.EdgeCount
== Contract.OldValue(ithis.EdgeCount) + (Contract.Result<bool>() ? 1 : 0));

*** The OldState value is evaluated after the preconditions.

Where to go next?

In the next post, I’ll show how to leverage these Contracts with Pex