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.


Leave a Reply

Your email address will not be published. Required fields are marked *