Continuing our series on Code Contracts. This time with the Contract.OldValue<T>() method. This method will return the value of the given variable at the start of the enclosing method or property. It is however only valid to use this method in a post conditional Contract.Ensures method call.

And that immediately indicates it’s purpose. It should be used to enable the use of post conditions that depend on the state of the world at method entry, compared to that at the return. For instance, if you would have a class with some collection or list functionality, you could have an Add method. The Contract.OldValue<T>() method enables you to check the count at method exit compared to the count at method entry. The following example shows this:

    public void Add(T item)
    {
      Contract.Requires(item != null);
      Contract.Ensures(this.innerList.Count == Contract.OldValue<int>(this.innerList.Count) + 1);
 
      this.innerList.Add(item);
    }

The count at method exit should match the old count incremented with 1 for the added item. There may be other uses for the Contract.OldValue(). Just remember, it may only be used in Contract.Ensures calls, which limits the use to post conditional checking. Any other checks on pre-entry state should be handcrafted by the programmers themselves. Another way of checking object state is the use of the Contract.Invariant method calls in a private method marked with the ContractInvariantMethod attribute. A description of those will follow in some future post in this series. Next post will deal with the Contract.ValueAtReturn<T>() method call.

That’s it for now
Meile