In a previous post we introduced Microsoft Code Contracts, and got an idea of what Design by Contract (DBC) is all about. It's now time to introduce another powerful concept that complements and completes preconditions and postconditions when you specify the behavior of your object: class invariants.
Invariants define all those conditions (or predicates, if you will) that are guaranteed to be true for all objects of a particular class throughout its life-cycle: these invariants need first to be met during construction and continue to hold before and after methods invocations.
Let's consider a very simple implementation of a class that represents a calendar date, specified by day, month and year:
Oversimplifying, such an object has some obvious invariants, or conditions that must always be met:
Yearmay not be negative
Daymust be a number between 1 and 31 (let's simplify and assume all months have the same days)
Monthmust be a number between 1 and 12
These conditions must be true upon successful creation of a
object and after each invocation of
With Code Contracts, one expresses invariants using a special method tagged
[ContractInvariantMethod] attribute; it is usually named
although this is just a convention: you can name it anything you like.
You are not allowed to put any other code but the invariants; the method must have
void return type and be protected (unless the class is sealed of course).
Invariants are checked at the end of every public method (including constructors and
excluding finalizers and methods implementing
IDisposable.Dispose()) - in
our example, every time a client of this class invokes the
the invariants will be checked.
Invariants, along with pre and postconditions, are inherited by subclasses. We'll see how this fits in a sound object oriented design in the next post.