University of Wyoming

Loop Invariants

RKHill; Last revised 31 August, 2000

Invariants should be well-formed formulas, that is, they should be
logical statements (with a truth-value--*true*, of course), in
the predicate calculus or rigorous English. A good invariant is a
*significant assertion about the current state of the process in
terms of the variables in the code or pseudocode*. An invariant
that repeats the source code is not useful, nor is one that bears no
obvious denotational relationship to the source code.

Consider a simple iterative loop (in C++ or Java) that finds the maximum element in an array A. Let's develop an appropriate invariant.

minidx = 0; for ( i=1; i<length; i++) //Invariant: if A[i-1] was less than A[minidx], minidx was set to i-1. if (A[i] < A[minidx]) minidx = i;

The version above is too close to the code, repeating precisely the
operations in the `if` statement.

minidx = 0; for ( i=1; i<length; i++) //Invariant: Least element so far has been found. if (A[i] < A[minidx]) minidx = i;

The second version is too far removed from the code; the "least element" mentioned is not associated with a program variable.

minidx = 0; for ( i=1; i<length; i++) //Invariant: Least element, A[minidx], is <= A[n], for all n from 0 to i-1. if (A[i] < A[minidx]) minidx = i;

The invariant above, although terse, is just right, providing useful information about the state of the program variables and even showing how the program segment is progressing toward its goal.

For another example, consider the insertion sort in Java, below. Two of the three loops are complex enough to warrant invariants, and good invariants are provided.

for (int i=1; i<size; i++) { // Invariant 1: A[0] to A[i-1] are sorted (relative to each other) int current = A[i]; int j = 0; while (current > A[j]) j++; for (int k=i; k>j; k--) // Invariant 2: current > A[i], for i from 0 to j-1, and current < A[k] A[k] = A[k-1]; A[j] = current; }

Invariant 1 describes the loop that gets the `i`th element to place it in order in the lower half of
the array. Therefore, all elements already passed by the index
`i` have been placed. Note the invariant is true
in all cases, including the first pass through the loop (vacuously),
when the range is simply `A[0]` to `A[0]`.

Invariant 2 is inside the loop that shifts the upper part of the
sorted array up to make room for the value `current`, which
belongs at the `j`th position,
determined in the previous statement. The invariant explains this by
incorporating variables from both the loop condition and the body.