Invariant code contracts – using class-wide contracts

It is possible to define invariant code contracts for classes. Invariant contracts should always hold true whatever member of class is called. In this posting I will show you how to use invariant code contracts so you understand how they work and how they should be tested.

This is my randomizer class I am using to demonstrate code contracts. I added one method for invariant code contracts. Currently there is one contract that makes sure that random number generator is not null.

public class Randomizer
{
    private IRandomGenerator _generator;
 
    private Randomizer() { }
 
    public Randomizer(IRandomGenerator generator)
    {
        _generator = generator;
    }
 
    public int GetRandomFromRangeContracted(int min, int max)
    {
        Contract.Requires<ArgumentOutOfRangeException>(
            min < max,
            "Min must be less than max"
        );
 
        Contract.Ensures(
            Contract.Result<int>() >= min &&
            Contract.Result<int>() <= max,
            "Return value is out of range"
        );
 
        return _generator.Next(min, max);
    }
 
    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(_generator != null);
    }
}

Invariant code contracts are define in methods that have ContractInvariantMethod attribute. Some notes:

• It is good idea to define invariant methods as private.
• Don’t call invariant methods from your code because code contracts system does not allow it.
• Invariant methods are defined only as place where you can keep invariant contracts.
• Invariant methods are called only when call to some class member is made!

The last note means that having invariant method and creating Randomizer object with null as argument does not automatically generate exception. We have to call at least one method from Randomizer class.

Here is the test for generator. You can find more about contracted code testing from my posting Code Contracts: Unit testing contracted code. There is also explained why the exception handling in test is like it is.

[TestMethod]
[ExpectedException(typeof(Exception))]
public void Should_fail_if_generator_is_null()
{
    try
    {
        var randomizer = new Randomizer(null);
        randomizer.GetRandomFromRangeContracted(1, 4);
    }
    catch (Exception ex)
    {
        throw new Exception(ex.Message, ex);
    }
}

Try out this code – with unit tests or with test application to see that invariant contracts are checked as soon as you call some member of Randomizer class.