Back in the mid to late sixties, academics were trying to rein in the increasing complexity of writing software. They felt there must be a scientific, mathematical, way to approach code.
In 1967, Robert Floyd wrote a paper about annotating flowcharts with logical assertions.1 Two years later, Tony Hoare build on this2 by describing how logical inference can be used to analyze (and in some cases verify) the execution of a program.
This was heady stuff, and the ideas are still used today in program proving systems and in specialized areas such as VLSI design.
However, there’s a less vigorous form of this theoretical work that we all use, every time we code. Often, though, we use it tacitly, If we can make it explicit, I think it will help us write better (and more accurate) code.
Conservation of Truth
Physicists have their four conservation laws: conservation of mass-energy, linear momentum, angular momentum, and electric charge. Using them, they can model and predict amazing consequences in the real world.
In software, we have our own conservation law:
Truth is neither created nor destroyed; it is just expressed differently
A program’s job is to transform truth into a more valuable form. A stack of transactions represents a truth. Organizing and analyzing them in a spreadsheet maintains that truth, but in a more usable form.
But that’s just an abstract idea. It turns out that the conservation of truth has a more practical consequence. And it is expressed in our designs by invariance.
What Must Be True
In an accounting system, debits must balance credits. That’s an invariant:
If we were writing an accounting system, we’d have a data store somewhere containing all the transactions. Each individual update to this store must maintain the invariant. At the same time that invariant is never expressed directly in code: it’s a a property of the state, not the code.
In object-oriented code, state is held in objects, and its structure is defined by those objects’ classes. So we’ve historically called this type of nonfunctional fact a class invariant. I personally prefer to call it a state invariant.
A state invariant imposes two constraints on our coding:
When a piece of state is first created, its state invariant must hold.
Every externally visible mutation of that state must preserve the invariant.
How does this affect design?
First, it tells us that all those classes that you see when you first construct an object and then make several calls to initialize it break state invariance. An object must meet its invariance constraints from birth.
Second, it tells us that every change to that object has to be atomic, and every change must maintain the invariant. This code is wrong:
Between the two calls, the state of the account is invalid: it doesn’t balance debits and credits. It would be better to do
That way, it is the responsibility of the account to maintain its invariant, and not that of the code that uses it.
This is a fundamental design goal: determine what must be true about a piece of state, and then localize the changes to that state to ensure that this truth can never be violated from the outside.
“not expressed in code…”
Earlier, I said that an invariant is never expressed directly in code. That’s largely true, but there are exceptions.
First, there are languages such as D that have support for specifying and verifying invariants. And, of course, there was Eiffel.
Design By Contract
In the late 80s, Bertrand Meyer created the language Eiffel. One of its ideas was to promote accurate programming through the use of contracts. In Eiffel, you could specify the invariant of a class, and it would check that this was not broken. It went further: you could also specify pre- and post-conditions on that class’s instance methods. If the precondition was met, the method would guarantee that the class invariant was preserved.
Here’s an example of Eiffel, stolen from Wikipedia:
The class invariant is down at the bottom: the day and hour must be within the given ranges. Each method has a require clause (the precondition) and an ensure clause (the post condition).
Eiffel never took off. Personally, I found it overly pedantic. But Meyer’s book, Object-Oriented Software Construction, had a profound impact on me, and forever changed the way I code.
Other Languages
Although your language most likely does not support class invariants, you can still implement them for special occasions.
I do this when I have critical data that I can’t afford to mess up. For these cases, I write a valid? method, and call it at the end of the public methods that change state. Do I leave it there during production? Of course: that’s when I really want to know if things are going haywire.
Other Invariants
There’s another kind of invariant I use every day while coding. And that will be the topic of another article…
A Challenge
The next time you write a class, or define a data structure, think about its invariants. What makes this data valid? Maybe even write a comment. Then, when you’re coding, make sure that none of your transformations of this data leave it in an invalid state.
Simply knowing that the invariant exists will make your code better.
What do you think? Do you see invariants when you write code?
Learning about Design by Contract forever changed how I write code.
It also provides a strong foundation for writing meaningful unit tests.