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.