Let's work through the process of reasoning about the loop invariant of an exponentiation (or power) function.
Exponentiation for nonnegative exponents is naturally defined as repeated multiplication: b^{0} = 1, and b^{e+1} = b * b^{e}. (b
is for base, e
is for exponent) We can write this recursive definition directly as a recursive function POW(b,e)
that computes b^{e}.
/* 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)
.
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.
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
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.
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.
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.
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.
(The exact same as before!)
Because we changed the loop body, this part changes. (TODO. See http://www.cs.cmu.edu/~fp/courses/15122-s11/recitations/recitation02.html)
(The exact same as before!)
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