C0 | Documentation
About Downloads Tutorial References Courses
C0 Tutorial C0 and other languages Other references

Reasoning with loop invariants

Let's work through the process of reasoning about the loop invariant of an exponentiation (or power) function.

Specification

Exponentiation for nonnegative exponents is naturally defined as repeated multiplication: b0 = 1, and be+1 = b * be. (b is for base, e is for exponent) We can write this recursive definition directly as a recursive function POW(b,e) that computes be.

/* pow1.c0 */

int POW(int b, int e) 
//@requires e >= 0;
{
  if (e == 0) {
    return 1;
  } else {
    return b * POW(b,e-1);
  }
}

This will be our specification function. The important lemmas about this function are that e == 0 implies that POW(b,e) == 1 and that e > 0 implies that POW(b,e) == b * POW(b,e-1).

Simple Implementation

Our objective is to use this specification function to establish the correctness of a function pow_iter that performs exponentiation using a while loop.

/* pow2.c0 */

/* 1  */ int pow_iter(int x, int y) 
/* 2  */ //@requires y >= 0;
/* 3  */ //@ensures \result == POW(x,y);
/* 4  */ {
/* 5  */   int accum = 1;
/* 6  */   int b = x;    
/* 7  */   int e = y;    
/* 8  */   while (e > 0)                 
/* 9  */     //@loop_invariant e >= 0; 
/* 10 */     //@loop_invariant accum * POW(b,e) == POW(x,y);
/* 11 */     {
/* 12 */       accum = accum * b;
/* 13 */       e = e - 1;
/* 14 */     }
/* 15 */   //@assert e == 0;
/* 16 */   return accum;
/* 17 */ }

Recall that a loop invariant is a condition that is true immediately before a loop condition is tested, both before you enter the loop and at the end of each iteration (if the loop runs).

Let's show that this function does return the correct result given its precondition (requires) and its loop invariants. For a function with one loop, this is a four part process. The first three parts establish partial correctness; the fourth part establishes termination.

Part 1: Show that the loop invariants hold before the loop condition is tested for the first time.

Just before the loop condition is tested for the first time, we know that accum = 1, b = x, e = y, and y >= 0. (Note: in C0, accum = 1 is a command that assigns accum to 1. However, when we reason mathematically, we will often write accum = 1 for equality, even though the test for equality is expressed in C0 with two equals signs, as accum == 1.)

Looking at the first invariant, we need to show accum * POW(b,e) == POW(x,y). We prove this by transforming the left side into the right side using what we know to be true about the values of variables and mathematical identities.

accum * POW(b,e) = 1 * POW(x,y)    (line 5)	
                 = POW(x,y)        (1 * x = x (multiplicative unit))

The second invariant we need to show is e >= 0. For this proof we use the information we know about y from the precondition.

y >= 0  (line 2)
e = y  (line 7)
 --> e >= 0

Part 2: If the loop invariants hold at the start of an iteration, show that they hold at the end of that iteration.

For this preservation property, we consider only one iteration or pass through the loop, not the entire execution of the loop.

First loop invariant

Looking at the first invariant, assume at the start of an iteration that:

e >= 0

Let e' be the updated value of e after the loop; we need to show that e' >= 0 to show that this first loop invariant was preserved.

e' = e - 1     (line 13)
e' + 1 = e     (add 1 to both sides)
e > 0          (line 8)
 --> e' + 1 > 0     

It's a fact of integer math that if e' + 1 > 0, then e' >= 0, so the first loop invariant is preserved.

Second loop invariant

To show the second loop invariant is preserved we assume accum * POW(b,e) == POW(x,y) and we have to show accum' * POW(b,e') == POW(x,y). (The values of b, x, and y are not changed by the loop.)

(Now, wait a minute! The POW function has a precondition, the second argument must be positive. Why are we allowed to call POW(x,y)? Because of line 2, y >= 0. Why are we allowed to call POW(b,e) and POW(b,e')? Well, because of line 9, e >= 0. The order of the loop invariants matters! Whenever we call a function with a precondition, like POW we have to be able to point to the reason we are allowed to call that function. In this case we point to lines 2 and 9.)

Back to the task at hand. We assume we're going through the loop body, which means we know that the loop guard, e > 0, is true.

POW(x,y) = accum * POW(b,e)       (assumed)
         = accum * b * POW(b,e-1) (lemma)
         = accum' * POW(b,e-1)    (line 12, accum' == accum * b)
         = accum' * POW(b,e')     (line 13, e' == e - 1)

This means accum' * POW(b,e') == POW(x,y), and so we know that the second loop invariant is preserved.

Before we move on, what have we shown so far? The invariants hold just before you enter the loop. They also hold at the end of each iteration if they hold at the start of each iteration. This implies that the invariants hold at the end of the first iteration (since the loop condition doesn't change anything in the invariant). But since the invariants hold at the end of the first iteration, they must hold at the start of the second iteration (again since the loop condition doesn't change any variable values). Thus, they must also hold at the end of the second iteration, and so on. What we've shown is that the loop invariant holds at the start and end of EVERY iteration.

Part 3: Show that if the loop terminates, we achieve our desired postcondition (given in the ensures annotation).

If the loop terminates, the loop invariants

e >= 0 && accum * POW(b,e) == POW(x,y)

should still hold (why?). What else holds? The negation of the loop condition must also be true. That is, !(e > 0), which is the same thing as saying e <= 0. What can we infer from this?

accum * POW(b,e) == POW(x,y) && e >= 0 && e <= 0
 --> accum * POW(b,e) == POW(x,y) && e == 0
 --> accum * POW(b,0) == POW(x,y)
 --> accum * 1 == POW(x,y)        (property of POW)
 --> accum == POW(x,y)            (multiplicative unit)

This says that immediately after the loop terminates, accum is equal to POW(x,y). But this is exactly what the function returns as specified by our ensures annotation, and the function performs no other operations after the loop terminates (other than returning the answer, accum), so we've shown that the function does return the correct answer... if the loop terminates.

Part 4: Argue that the loop terminates.

To prove that the function terminates, we need to convince ourselves that e <= 0 after a finite number of loop iterations. But this is easy, as e just counts down by one in every iteration of the loop.

Fast implementation

It's important to realize that all the parts of this argument are separable. When we're reasoning about Part 1 and Part 3, it doesn't matter how the loop invariants are preserved. We can even swap out the body of the while loop with some completely different function, as long as it preserves the loop invariants!

/* pow3.c0 */

/* 1  */ int pow_fast(int x, int y) 
/* 2  */ //@requires y >= 0;
/* 3  */ //@ensures \result == POW(x,y);
/* 4  */ {
/* 5  */   int accum = 1;
/* 6  */   int b = x;    
/* 7  */   int e = y;    
/* 8  */   while (e > 0)                 
/* 9  */     //@loop_invariant e >= 0; 
/* 10 */     //@loop_invariant accum * POW(b,e) == POW(x,y);
/* 11 */     {
/* 12 */       if (e % 2 == 1)
/* 13 */	 accum = b * accum;
/* 14 */       b = b * b;
/* 15 */       e = e / 2;
/* 17 */     }
/* 18 */   //@assert e == 0;
/* 19 */   return accum;
/* 20 */ }

Parts 1 and 3 of our correctness reasoning can stay exactly the same - the loop invariants hold before the loop condition is tested for the first time for the same reason as before, and if the loop terminates, we achieve our desired postcondition for the same reason as before. But we do have to reason about part 2, preservation, because the loop body changed. We also have to revise our argument for termination.

Part 1: The precondition implies the loop invariant

(The exact same as before!)

Part 2: Preservation

Because we changed the loop body, this part changes. (TODO. See http://www.cs.cmu.edu/~fp/courses/15122-s11/recitations/recitation02.html)

Part 3: The loop invariant and the negation of the loop guard together imply the postcondition

(The exact same as before!)

Part 4: Termination

To prove that the function terminates, we again need to convince ourselves that e <= 0 after a finite number of loop iterations. One way to show this is to prove that e is strictly decreasing on each execution of the loop. In this example, e is divided by 2 each time through the loop, so we need to prove e/2 < e. Since integer division rounds down, we know this is true. Formally, we can prove this by analyzing the even and odd cases:

In either case, we know that we entered the loop, so e > 0

  • e is even, so e = 2f for f < e (strictly greater because e > 0). Then e/2 = 2f/2 = f < e.
  • e is odd, so e = 2f+1 for f < e (strictly greater because e > 0). Then e/2 = (2f+1)/2 = f < e.

written by Tom Cortina, 1/14/11
revised by Rob Simmons, 8/30/12