Invariants are a kind of postconditions which apply to all members. How to formulate them using Code Contracts?
In the previous part we got started using Microsoft Code Contracts and formulated first pre- and postconditions. We only looked at “simple” ones. In this posting you will learn what object invariants are and how they are connected with Code Contracts.
What are Invariants?
As anticipated in the introduction, invariants can be compared to postconditions valid for all members of a class. In fact, you are actually able to modulate them using Contract.Ensures(invariant) in each member.
However, they are more than simple postconditions – they are always valid, regardless of the object’s state. So invariants must never be broken during an object’s lifetime. Thus, other members can rely on them like on preconditions.