Last week, I discussed how Dijkstra used a loop invariant to help understand the power function, which we expressed as

double power(double x, unsigned n)

{

    assert(n != 0 || x != 0);
    double r = 1;




// Invariant: Our desired result is r * xn




    while (n != 0) {

         r *= x;

         --n;

    }

    return r;
}

This code is an example of a typical strategy: We start with an unsigned integer, here called n, that we reduce to zero while maintaining an invariant. The invariant is such that once n has become zero, we will know the result that our code intends to compute. In this particular case, that result will be in the variable r.

The most straightforward way to reduce n to zero in a loop is to decrease n by 1 as long as n is not zero. However, there are other ways to reduce n more quickly. In particular, Dijkstra observed that if n is even, we can divide it by 2 and get an exact integer result. Because xn is equal to x(n/2) * x(n/2), we can restore the invariant simply by squaring x. In other words, we can rewrite our code as

double power(double x, unsigned n)

 {

     assert(n != 0 || x != 0);
        double r = 1;


        // Invariant: Our desired result is r * xn

        while (n != 0) {

           while (n % 2 == 0) {
               x *= x; // Break the invariant
               n /= 2; // Restore the invariant
           }
           r *= x; // Break the invariant

           --n; // Restore the invariant
        }
    return r;
}

We now have two nested loops with the same invariant. Each loop assumes that the invariant is true at the beginning of each trip through the loop; each loop decreases n while maintaining the invariant. The difference between the two is that the inner loop reduces n by a factor of two each time through, whereas the outer loop decreases n by one each time. Accordingly, there is no guarantee that n will be zero when the inner loop terminates — but such a guarantee is unnecessary. All that is necessary is to ensure that n has not increased during the loop. Because the only operation that the inner loop performs on n is to divide it by 2, that condition is easily met.

To prove that the inner loop terminates, we can add a second invariant to the inner loop: n != 0. We know that this invariant is true when we enter the inner loop for the first time because the condition of the outer loop ensures it. We also know that each time through the inner loop, n is even, because the condition of the inner loop ensures it. Therefore, when we divide n by 2, the result is exact; and dividing a nonzero value by 2 to yield an exact result cannot ever yield zero.

Using this inner invariant to prove that n is never zero in the inner loop helps us in two ways. First, it means that the inner loop must terminate. If it were possible for n to be zero, we might get in trouble; the loop might run forever with n being zero each time through. But if we start with an integer greater than zero, and we divide it by two enough times, we will eventually reach an odd value and the loop will stop.

The second way in which the inner invariant helps us is to ensure that when the loop terminates, n is still not zero, because zero is an even number. As a result, when we decrement n at the end of the outer loop, we know that the result cannot be negative.

Each of our loops decreases n while maintaining the invariant. The inner loop decreases it quickly, but in a way that might not cause it to reach zero. The outer loop does so more slowly, but in a way that guarantees that n will eventually become zero. As a result, we are still assured that the program will yield the right result, and we have good reason to believe that in many cases, the program will run more quickly than the original.

What I find remarkable about this program is that the invariant makes it unnecessary to answer what one might think is an obvious question: What is the value of r at each point in the code? We don't need to know the exact value of r; we need only to know that r has whatever value will ensure that our eventual result is r * xn. In other words, we care not about the value of r but about its properties. In effect, an invariant is an abstraction that allows us to ignore the exact value of a variable while still reasoning about the program.

Next week, I intend to talk about how invariants can help us test our programs, after which I shall apply invariants to a trickier problem than this one.