8.6. Loop Invariants

When planning an algorithm that uses a loop, it can help to think about the values of variables as they are each time the loop reaches its beginning. As an example, let's rewrite the function that computes n! Here is a suggestion for variable values for the example where n = 5.

1. At each line, r = k!. For example, in one of the lines k = 4 and r = 24. Notice that 4! = 24. The assertion that r = k! is called a loop invariant.

2. The first line is chosen to make it easy to choose values that make the loop invariant true. We know that 1! = 1.

3. The lines gradually change k so that it eventually becomes n.

4. The last line contains the answer in r. Notice that, in the last line, k = n (since this was for the example n = 5). Since we have arranged for r = k! to be true at every line, and k = n in the last line, it must be true that r = n! in the last line.

Now write the algorithm using a while-loop. First, initialize the variables as indicated in the first line of the table. Keep going until reaching the last line of the table (where k = n). The loop body must update k and r appropriately to change them to the values in the next line, ensuring that the loop invariant is once again true.

  //===============================================
  // factorial(n) returns n!.
  //===============================================

  long factorial(long n)
  {
    long r = 1;
    long k = 1;
    while(k != n)
    {
      k = k + 1;
      r = r * k;
    }
    return r;
  }

In general, a loop invariant is an assertion about the current values of the variables that is true each time the algorithm gets to the top of a loop. A loop invariant does not tell how variables will change over time; it only discusses their current values.

Loop invariants are part of the study of how to prove that an algorithm involving a loop works. Once you have identified the loop invariant that you believe is correct, it is just a matter of (1) showing that the loop invariant is true for the initial values of the variables, and (2) showing that, if the loop invariant is true just before the loop body is run, then it is also true after the loop body runs. Here are proofs for the factorial function.

1. Initially, k = 1 and r = 1. Since 1! = 1, the invariant is true the first time the loop reaches its start.

2. Suppose that r = k!. Imagine performing the loop body. It modifies r and k. Let's use r′ and k′ for the modified, or updated, values of r and k. According to the loop body, it is evident that

   k′	=	k + 1
   r′	=	r * k′

In words, the new value of k is one larger than the old value of k. The new value of r is the old value of r times the new value of k. Let's check whether the loop invariant is true for the new values, r′ and k′. That is, is r′ = (k′)!?

  r       = k!                (given)
  r*(k+1) = k!*(k+1)          (multiply both sides by k+1)
  r*(k+1) = (k+1)!            (since (k+1)! = k! * (k+1))
  r*k′    = (k′)!             (since k′ = k+1)
  r′      = (k′)!             (since r′ = r*k′)

Finally, notice that the while-loop ends when it sees that expression k ≠ n is false. That is, when it ends, k = n. The program gets out of the loop and hits the return statement. But no variables changed between noticing that k = n and getting to the return statement. So k must still be equal to n at the return statement. Since the loop invariant was true at the top of the loop, it must also be true at the return statement (again, since the values of the variables did not change.) We conclude that, at the return statement, r = n!.