Code Contracts – Invariants

Compared to pre-conditions and post-conditions, invariants might seem like a quite different concept. Unlike the above mentioned contract types, invariants do not apply to methods but are used to verify the state of a class instance.

A class can contain multiple fields and properties that carry various information regarding the instance state and behavior. Invariants are used to make sure that every instance of the class that implements a contract is following the “directives” set by the contract, therefore satisfying the contract.

For example, there is the Car class:

class Car
{
    public bool isWorking;
}

Obviously this is a very simple class and in practice you will work with way more complicated stuff, but to illustrate the use of invariants, it is perfect. The isWorking value represents whether the car (represented by the Car instance) is working or not.

Now, I am also creating a method that will change the state of the instance at random:

public void ChangeState()
{
    Random random = new Random();
    double result = random.NextDouble();
    isWorking = Convert.ToBoolean(Math.Round(result));
}

I am using this to demonstrate that the contract will either fail or succeed depending on the state of isWorking. But so far – there is no contract.

For invariants, a single contract method should be introduced inside the class that will check the state of an instance. This method should be decorated with the ContractInvariantMethod attribute. Although not required, I highly recommend having only one such method inside the class.

No exception will be thrown if you use several methods with set to check the state, but this later on leads to performance issues – it is tied to how the process is taking place. Take a look at the diagram:

Once the object instance is initialized, every method set as ContractInvariantMethod inside the class is automatically triggered to check the state of the object. For every method included in the object, that is executed, the contract methods are once again triggered to check the state of the object. You can imagine how it affects the performance if several state checkers are being run once a single method is called, especially if there are multiple conditions and complex methods.

Now to the actual invariant method implementation. My method looks like this:

[ContractInvariantMethod]
void CheckState()
{
    Contract.Invariant(isWorking);
}

Simple enough, it is using Contract.Invariant to check against a Boolean value. It can be a stament that results in a Boolean value, but in my case I am just checking an existing field. The method should be void and not contain any other code than Invariant calls.

NOTE: There is an overload for Invariant that allows you to set a message once the contract fails. All you have to do is add a second parameter that is a string.

Invariant methods are implicitly called at runtime, therefore you don’t have to write any additional calls. In case it is called, an error will show up:

NOTE: Invariant methods are not triggered if a method that implements System.IDisposable.Dispose (member of the class) is triggered.

Once the class is set, I am initializing an instance of it and call the ChangeState method.

Car car = new Car();
car.ChangeState();

I am not sure how the state value will be, since it is random, so running the program a couple of times will eventually result in satisfied and failed contracts.