The loop condition is evaluated, and again it is true. This time, since the
rightmost bit of the binary representation of y is 0 , y is even, and the then-part is
executed. The then-part divides y by 2 . Division of an even decimal number by
2 is equivalent to deleting the last 0 of its binary representation, yielding 10.
Again, the loop condition is evaluated, and again it is true. Again, y is even,
and the then-part is executed. This statement divides y by 2 . This deletes the last
0 of its binary representation, yielding 1.
Again, the loop condition is evaluated, and again it is true. y is odd, and the
else-part is executed. This statement subtracts 1 from y , yielding 0 . This termi-
nates the loop.
This analysis should convince you that this algorithm processes the binary
representation of exponent y . The loop iterates once or twice for each bit of the
exponent, so the total number of iterations is bounded above by twice the num-
ber of bits in the binary representation of the exponent. So, to compute 2 15
requires at most 8 iterations ( 15 in binary is 1111 ) and to compute 2 127 requires
at most 14 iterations ( 127 in binary is 1111111 ). Compare this with the slow ver-
sion in Fig. 7.1a, which requires 127 iterations to calculate 2 127 !
page 7-2 to ob-
tain this loop
Using the invariant
Focusing on y has enabled us to determine the maximum number of itera-
tions of the loop and has given us insight into how y is used. But it hasn't helped
us determine that the loop is correct. How do we know that z has the correct
value upon termination?
We know of no way of explaining this without using the invariant, which
gives the relation between all five variables of the algorithm.
From our earlier analysis, we can see that the second conjunct of the invari-
ant, 0≤y≤c , is true initially and is maintained by the repetend. So, we concen-
trate on the first conjunct, z*x y = b c .
How does it start? To see that the first conjunct of the invariant is true ini-
tially, make a copy of the conjunct and, because of the initialization, replace each
occurrence of x with b , of y with c , and of z with 1 to yield 1*b c =b c , which
is true. So, the initialization truthifies the conjunct.
When can it stop? It stops when y=0 . Substituting 0 for y in invariant z*
x y =b c yields z*x 0 =b c , which reduces to z=a b because x 0 =1 .
How does it make progress? Each iteration either decreases y by 1 or
halves y , making y closer to 0 .
How does it fix the invariant? Checking that the repetend maintains the
invariant requires looking at two cases: y is odd or y is even.
For the case that y is even, we use this identity:
x y = (x * x) y/2 (for y even)
Therefore, the assignments to x and y keep the value of x y the same, so the value
of the first conjunct remains unchanged.
For the case that y is odd, we use this identity: