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.
-
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 r = 1, b = x, e = y, and y >= 0.
Looking at the first invariant, we need to show
r * 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.
r * pow(b,e) == 1 * pow(x,y) (by substitution)
1 * pow(x,y) == pow(x,y) (1 * x = x (multiplicative identity))
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 (@REQUIRES)
e >= 0 (since e = y)
-
Show that the loop invariants hold just before the loop condition is tested
after each iteration. Equivalently: if the loop invariants hold at the start
of an iteration, show that they hold at the end of that iteration. (Consider
only one iteration or pass through the loop, not the entire execution of the loop.)
Looking at the first invariant, assume at the start of an iteration that:
r * pow(b,e) == pow(x,y)
There are two cases to consider here.
-
Consider the case where e is even. If e is even, we can
say that e = 2f for some integer f. (That is, e
is two times some other integer for it to be even.)
Show that r' * pow(b',e') == pow(x',y') where variables with
primes (') indicate the new values of the variables at the end of that
iteration.
Since e is even, the if statement does not change r
so at the end of the iteration, we know that:
r' = r
b' = b * b
e' = e / 2 = 2f / 2 = f
x' = x
y' = y
Now we show that the invariant after the loop runs is true after one iteration
if we assume it is true before that iteration runs:
r' * pow(b',e') == r * pow(b*b,f) (by substitution)
r * pow(b*b,f) == r * pow(b,2f) (by definition of a^b)
r * pow(b,2f) == r * pow(b,e) (by substitution)
r * pow(b,e) == pow(x,y) (from loop invariant)
pow(x,y) = pow(x',y') (by substitution)
What we're showing is that the invariant after the iteration is true as long
as the invariant holds before that iteration.
Looking at the other invariant (when e is even), we need to show
that e' >= 0 assuming e >= 0.
e >= 0 (from loop invariant)
2f >= 0 (by substitution)
f >= 0 (by definition of integer division)
e' >= 0 (by substitution)
So we've shown that the loop invariants hold at the end of an iteration if they
hold at the start of an iteration and e is even.
-
Consider the case where e is odd. If e is odd, we can
say that e = 2f + 1 for some integer f. (That is, e
is two times some other integer plus 1 for it to be odd.)
Show that r' * pow(b',e') == pow(x',y').
Since e is odd, the if statement does change r
this time so at the end of the iteration, we know that:
r' = r * b
b' = b * b
e' = e / 2 = (2f + 1)/ 2 = f (WHY?)
x' = x
y' = y
Now we show that the invariant after the loop runs is true after one iteration
if we assume it is true before that iteration runs:
r' * pow(b',e') == r * b * pow(b*b,f) (by substitution)
r * b * pow(b*b,f) == r * b * pow(b,2f) (by definition of a^b)
r * b * pow(b,2f) == r * pow(b,2f+1) (by definition of a^b)
r * pow(b,2f+1) == r * pow(b,e) (by substitution)
r * pow(b,e) == pow(x,y) (from loop invariant)
pow(x,y) = pow(x',y') (by substitution)
We also have to show that e' >= 0 if e >= 0 when e
is odd.
e >= 0 (from loop invariant)
2f+1 >= 0 (by substitution)
f >= 0 (by definition of integer division)
e' >= 0 (by substitution)
So we've shown that the loop invariants hold at the end of an iteration if they
hold at the start of an iteration and e is odd.
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.
-
Show that if the loop terminates, we achieve our desired postcondition (given
in the ensures annotation).
If the loop terminates, the loop invariants
r * pow(b,e) == pow(x,y) && e >= 0
should still hold (why?).
What else holds? The negation of the loop condition must also be true.
That is, !(e > 0) == e <= 0.
What can we infer from this?
r * pow(b,e) == pow(x,y) && e >= 0 && e <= 0
r * pow(b,e) == pow(x,y) && e == 0
r * pow(b,0) == pow(x,y)
r * 1 == pow(x,y)
r == pow(x,y)
This says that immediately after the loop terminates, r 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), so we've shown that
the function does return the correct answer... if the loop terminates.
- 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. 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.
So we've shown that given the precondition, we can use
the loop invariants to show that the postcondition follows and that
the function is correct.