Code Contracts: Invariants

In a previous post we introduced Microsoft Code Contracts, and got an idea of what Design by Contract (DBC) is all about. It's now time to introduce another powerful concept that complements and completes preconditions and postconditions when you specify the behavior of your object: class invariants.

Invariants define all those conditions (or predicates, if you will) that are guaranteed to be true for all objects of a particular class throughout its life-cycle: these invariants need first to be met during construction and continue to hold before and after methods invocations.

Let's consider a very simple implementation of a class that represents a calendar date, specified by day, month and year:

public class Date
{
  public short Day { get; }
  public short Month { get; }
  public short Year { get; }

  public Date(short dd, short mm, short yy)
  {
    Day = dd;
    Month = mm;
    Year = yy;
  }

  public void Increment()
  {
    // some tricky code to increment the day,
    // month (if needed) and year (if needed)
  }
}

Oversimplifying, such an object has some obvious invariants, or conditions that must always be met:

• Day, Month, and Year may not be negative
• Day must be a number between 1 and 31 (let's simplify and assume all months have the same days)
• Month must be a number between 1 and 12

These conditions must be true upon successful creation of a Date object and after each invocation of Increment().

With Code Contracts, one expresses invariants using a special method tagged with a [ContractInvariantMethod] attribute; it is usually named ObjectInvariant although this is just a convention: you can name it anything you like.

public class Date
{
  // ...
  // rest of the class as listing above

  [ContractInvariantMethod]
  protected void ObjectInvariant()
  {
    Contract.Invariant(this.Day >= 0);
    Contract.Invariant(this.Day <= 31);
    Contract.Invariant(this.Month >= 0);
    Contract.Invariant(this.Month <= 12);
    Contract.Invariant(this.Year >= 0);
  }
}

You are not allowed to put any other code but the invariants; the method must have a void return type and be protected (unless the class is sealed of course).

Invariants are checked at the end of every public method (including constructors and excluding finalizers and methods implementing IDisposable.Dispose()) - in our example, every time a client of this class invokes the Increment() method, the invariants will be checked.

Invariants, along with pre and postconditions, are inherited by subclasses. We'll see how this fits in a sound object oriented design in the next post.