Last week, I described the proof technique called mathematical induction. Reduced to essentials, that technique is:

• We wish to prove that a claim P(n) holds true for every natural number n.
• We prove that P(0) is true.
• We prove that whenever P(n) is true for a particular natural number n, P(n+1) is also true.

By completing these two subproofs, we have proven that P(n) is true for every natural number n.

Suppose we want to prove that a program has a particular property — for example, that it produces the right answer. What makes such proofs hard is that we typically do not know in advance how many times the loops in our programs will execute. As a result, it is hard to describe the program's behavior during a particular execution, because we do not know exactly what it will do as it executes.

It is often possible to avoid such difficulties by proving the desired properties of our program by induction. We let n represent the number of times a loop executes, and then we prove by induction that the program is correct for all values of n.

According to our description of induction, such a proof looks like this:

• We prove that the program works correctly at least up to the point where the loop is about to begin executing for the first time (i.e., we prove P(0)).
• We prove that if the program has worked correctly for n iterations, it will work correctly for n+1 iterations.
• By completing these two subproofs, we have proven that P(n) is true for every natural number n — in other words, that the program will work correctly no matter how many iterations the loop executes.

Of course, the notion that "the program works correctly" is vague. We can make it less so by writing down a specific claim that applies to our particular loop. Such a claim is called a loop invariant. To make this discussion concrete, let's revisit the code fragment that I introduced on August 18:

 
double sum(double* begin, double* end)
{
      double result = 0;
      double* p = begin;
      while (p != end) {
           result += *p;
           ++p;
      }
      return result;
}
 

I want to look particularly at the while loop and invite you to think about how we might frame the proposition that the program works correctly. What this loop does is to compute the sum of the elements in the range [begin, end) (i.e., the elements in the sequence of locations starting at *begin and extending up to but not including *end). As the loop executes, we have a pointer p that indicates how much progress we have made. Accordingly, we expect that at the beginning of each trip through the loop, result should hold the sum of the elements in the range [begin, p). We can express that expectation as an invariant, which we shall write as a comment:

double sum(double* begin, double* end)
{
      double result = 0;
      double* p = begin;
 
      // Invariant: result is the sum of the elements in [begin, p) .
      while (p != end) {
           result += *p;
           ++p;
      }
      return result;
}
 

We now go through the three steps of the proof.

First, we show that before the loop begins executing, the invariant is true. We can see this because p is equal to begin, which makes the range [begin, p) empty. The sum of an empty range is zero, which is the value that we have given to result.

The next step is to assume that the invariant is true at the beginning of a trip through the loop and prove that it is still true at the end. We do so by observing that the statement

 
result += *p;

causes result to be the sum of the elements in [begin, p) and the element at *p, which is equivalent to the sum of the elements in [begin, p]. (Note the square bracket at the end of the range; this bracket indicates that the range includes, rather than excludes, the element to which p points.) In other words, the invariant is now false.

However, when we increment p, the range that [begin, p] formerly represented is now represented by [begin, p). By incrementing p, we make the invariant true again.

We have now proved by induction that no matter how many times the loop executes, the invariant will be true even after the loop exits. Moreover, when the loop eventually does exit, we also know that p is equal to end, because we imposed that requirement by our choice of condition in the while statement. This fact, combined with the invariant, proves that when the loop terminates, result is the sum of the elements in [begin, end).

This example suggests a general technique for writing loops:

• Define an invariant that describes the loop's behavior, independently of how many times it executes.
• Choose a condition for the while statement that, when combined with the invariant, yields the behavior we want. Write the body of the loop in a way that maintains the invariant while working toward eventually making the while condition false, so that the loop will always terminate.

This technique is useful in a wide variety of contexts, and is even useful as an informal way of talking about how programs work (or are intended to work). Next week we shall discuss a beautifully elegant example that Dijkstra used to illustrate this technique.