Software Invariants

An invariant is a fact or proposition about the data that a program manipulates that remains true even as the program runs. I do not know who invented the idea or who named it but I remember being struck at its novelty when I heard it, and only later by its utility.

I still recall the first invariant I heard described. A very simple machine language loop to compute the sum of an array of 100 integers. 

   R2 ← address of array
   R3 ← 100
   R1 ← 0
L: R1 ← C(R1) + C(C(R2))
   decrement R3
P: increment R2
   goto L unless C(R3) = 0
The first invariant is:
If C(PC) = L then (C(R1) plus the sum of the numbers in memory locations between C(R2) and the end of the array, inclusive) is the sum of the entire array.
or
If C(PC) = L then C(R1) is the sum of the numbers in the array before location C(R2).
Not everything is precise here but the reader may be convinced that it could be made much more precise, even to the point where a computer program could understand the claim. Further invariants could be formed beginning “If C(PC) = P then” and several more such invariants would reach the point where axioms of machine semantics would yield a formal correctness proof.

The point of this exercise is not to be even more sure that the program is correct, but to see a connection between the world of static mathematical platonic objects, its axioms and theorems, and the world of real electronic computers. An invariant is a ‘what is’ comment about a ‘how to’ construction such as a computer program. I understood that the program was correct before. I know no way to understand balanced tree algorithms, however, than first to understand the invariants.

The introduction of this paper gives a quick description of the rationale of invariants. It goes on to describe how to automatically find candidate invariants in some given program.
Here is a special case called a “representation invariant” which is a proposition that holds except while a method of an abstract data type is running. It uses invariants to describe the logic of a balanced tree.
Some brief notes on Keykos kernel invariants.