Department of Computer Science
University of Wyoming

Loop Invariants

RKHill; Last revised 4 April, 2019

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 (index of the) minimum 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, at 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;

The insertion sort proceeds as follows in this partial example, showing some states of the inner loop cycle where i = 3
254158386719  current=38, k=3
254141586719  ...moving values up to A[k]
253841586719  ...current is placed correctly

Invariant 1 describes the loop that gets the ith 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 jth position, determined in the previous statement. The invariant explains this by incorporating variables from both the loop condition and the body.

Robin Hill 20190404