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) = 0The 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.