Loops Invariants, Correctness, and Program Derivation

A loop invariant is a relation among program variables that is true when control enters a loop, remains true each time the program executes the body of the loop, and is still true when control exits the loop. Understanding loop invariants can help us analyze programs, check for errors, and derive programs from specifications.

A first example

Here is a simple example. This Java method named sum is a function that returns the sum of the elements in array a, its argument. It uses the local variable s to accumulate the sum and uses i to index the array elements.


    public static int sum(int a[]) {

	int s = 0;

	for (int i = 0; i < a.length; i++) {

	    // s is the sum of the first i array elements

	    // s == a[0] + .. + a[i-1]

	    s = s + a[i];

	}

	return s;

    }

The comments in the loop body describe the invariant. The first comment describes the invariant in English: s is the sum of the first i array elements. The second comment expresses the invariant in a form similar to a Java boolean expression: s == a[0] + .. + a[i-1]. This form emphasizes that the invariant is an assertion, an expression that should always evaluate to true (the two dots .. used here to indicate the other terms in the sum are not legal Java syntax).

The invariant expresses a relation between the three variables s, i, and a that remains true even when the values of s and i change: s is always the sum of the first i elements in a. When control enters the loop, i is 0 so s is the sum of no array elements. When control exits the loop, i is a.length, so s is the sum of all of the array elements. This is the intended result.

This simple example shows why thinking about loop invariants can help us write programs. When the program exits a loop, the loop invariant expresses the intended value(s) of the variable(s) at that point. Therefore we can work backwards from the intended values to the loop invariant, and then to the code itself. This can be a systematic method for writing programs which can supplement the usual method of relying on intuition and lots of trial-and-error. Programs derived in this way can be surprising and unobvious --- the kind that make you wonder, "How did they come up with that?"

Making it clearer

It is necessary that the loop invariant be true on each iteration before executing the body of the loop, and again after executing the body. In our example, the body of the loop is the statement s = s + a[i], followed by i++ (because the third expression in the for statement is actually executed at the end of the body of the loop, each time the body is executed). The first time the program executes the loop, i == 0 and sum == 0 before executing the body, and i == 1 and sum == a[0] after executing the body. Both situations satisfy the invariant.

The for loop makes it a bit difficult to see what's going on because the statement which is actually executed at the end of the body of the loop (i++ in our example) doesn't appear there, it appears in the for statement itself. For the purposes of understanding and deriving loops, it is often clearer to express a for loop as the equivalent while loop.

Here is how to transform a for loop to the equivalent while loop. This for loop


   for (s; p; u) {

      t;

   }

is equivalent to this while loop


   s;

   while (p) {

      t;

      u;

   }

So our example code can be transformed to


    public static int sum2(int a[]) {

	int s = 0, i = 0;

	while (i < a.length) {

	    // s is the sum of the first i array elements

	    // s == a[0] + .. + a[i-1]

	    s = s + a[i];

	    i = i + 1;

	}

	return s;

    }

Understanding loops

We need a few more definitions.

The guard is the boolean expression that determines whether to execute the body of the loop. The program executes the body of the loop as long as the guard is true. In a while loop, the guard is the boolean expression that occurs in the while statement (in a for loop, the guard is the second expression in parentheses in the for statement). In this example, the guard is i < a.length.

The variant is a numeric expression that measures how much work is left to do. Usually the variant does not occur explicitly in the code, you must infer it. Quite often the variant is simply the number of loop iterations that remain to be done. In our example, the variant is a.length - i.

Now we have all the concepts we need to understand loops. A loop is correct if the five conditions in this checklist are all true:

  1. Initialization: the invariant is true before entering the loop
  2. Invariance: the body of the loop preserves the invariant
  3. Progress: the body of the loop decreases the variant.
  4. Boundedness: when the value of the variant falls below some threshold, the guard becomes false.
  5. Exit: the negation of the guard and the invariant describe the goal.

We can confirm all five conditions in our example:

  1. Initialization: i == 0 && s == 0 before entering the loop
  2. Invariance: executing the body of the loop gives i == 1 && s == a[0], then i == 2 && s == a[0] + a[1], etc.
  3. Progress: when we execute the body of the loop, the statement i = i + 1 decreases the variant a.length - i.
  4. Boundedness: when the value of the variant falls below 1, the guard i < a.length becomes false.
  5. Exit: The negation of the guard i == a.length and the invariant s == a[0] + .. + a[length-1] describe the goal.

Exercises

Before we go on, let's check our understanding of invariants. For each of these code samples, see if you can express the loop invariant in English and in symbols (as a Java boolean expression, or as near to one as you can write).

This code computes the power xn by repeated multiplication:

	  

    public static int power(int x, int n) {

	int p = 1, i = 0;

	while (i < n) {

	    p = p * x;

	    i = i + 1;

	}

	return p;

    }

This code performs integer division by repeated subtraction. It divides numerator n by divisor d, returning quotient q and also calculating remainder r. To understand this code, it is useful to understand this definition for for integer division that relates relates the outputs q and r to the inputs n and d:   r < d && n = q*d + r


    public static int quotient(int n, int d) {

	int q = 0, r = n;

	while (r >= d) { 

	    r = r - d;

	    q = q + 1;

	}

	return q;

    }

These exercises are a little contrived. As we shall see, it is usually more effective to start with the loop invariant and derive the code from that.

Deriving loops

We can derive loops by considering the general pattern that relates the code in the loop to the assertions. Here I is the invariant, P is the guard, S is the code that precedes the loop and Tis the code in the body of the loop:


   S

   // I 

   while (P) {

      // I 

      T

      // I 

   }

   // !P && I 

This shows that the assertion !P && I will be true when code exits the loop. This is called the postcondition (because it is true after executing the loop).

Let's look again at integer division. Now we know enough to derive the code from the definition r < d && n == q*d + r. We want this definition to match the postcondition !P && I. We notice that !P in the postcondition matches r < d in the definition, and the invariant I matches n == q*d + r. We can derive the guard P by negating r < d to obtain r >= d. Filling in the assertions, we now have:


   S

   // n == q*d + r 

   while (r >= d) {

      // n == q*d + r 

      T

      // n == q*d + r 

   }

   // r < d && n == q*d + r 

Now we have to derive the code fragments S and T. The basic idea is to count how many times we can subtract the divisor d from the numerator n. The quotient q is the counter, and remainder r is what remains after the subtraction.

Our first job is to write S, the startup code that initializes q and r. S has to establish the invariant I. It seems reasonable to start with r = n; q = 0;. Substituting these values into I, we obtain n == 0*d + n which is true. Checking S against I in this way gives us confidence that our code is correct.

Our next job is to write T, the body of the loop. T must preserve the invariant I. It seems reasonable to try r = r - d; q = q + 1. So, for example, after the first time we execute the loop body we'll have r == n - d && q == 1 (why?). Plugging these values back into I we obtain n == 1*d + n - d which is true. And so on, each time we execute the body of the loop. Again, checking T against I shows that our code is correct. We have derived


   r = n;   

   q = 0; 

   // n == q*d + r 

   while (r >= d) {

      // n == q*d + r 

      r = r - d; 

      q = q + 1;

      // n == q*d + r 

   }

   // r < d && n == q*d + r 

If you wish, you can use Java coding tricks to express this in a more compressed form:


   for (r = n, q = 0; r >= d; q++) r -= d;

Exercises

Consider the code for xn in the previous exercise. Write the boolean expressions for the guard P and the invariant I. Annotate the code with assertions and confirm to your satisfaction that the assertions are correct.

A boolean expression that defines the integer square root r of non-negative integer n is r*r <= n && n < (r+1)*(r+1). Derive a function sqrt that takes argument n and returns its root r (the easiest algorithm simply counts up to r).

References

My favorite book on program derivation is Programming in the 1990s: An Introduction to the Calculation of Programs by Edward Cohen, Springer 1990. There are other good books by Dijkstra, Gries, and Kaldewaij.


Jon Jacky, jackyj@evergreen.edu