Java Reference
In-Depth Information
iteration multiplies z by b and decrements
y
. For purposes of comparison with
the second version, we discuss this algorithm using the four loopy questions.
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 initializations, replace
each occurrence of
y
with
c
and
z
with
1
. This yields
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*
b
y
=b
c
yields
z*b
0
=b
c
, which reduces to
z=b
c
.
How does it make progress?
Each iteration decreases
y
by
1
, making
y
closer to
0
.
How does it fix the invariant?
To check that the repetend maintains the
invariant, we notice that we can “pull out” a factor of
b
:
z*b
y
= z*b*b
y-1
Therefore, the assignments to
z
and
y
keep the value of
z*b
y
the same, so the
value of the first conjunct remains unchanged. Thus, the repetend keeps the
invariant true.
Notice that
y
starts with value
c
,
y
decreases by one every iteration, and the
loop terminates when
y=0
. Thus, this loop takes
c
iterations.
Processing the binary representation of the exponent: how fast?
We first analyze how quickly the loop in Fig. 7.1b terminates. Then, we dis-
cuss its correctness.
The loop uses information about the binary representation of exponent
c
.
For example, suppose
c
is
5
, which is
101
in binary. The second statement
assigns (binary)
101
to
y
. Because
y
is not
0
, the repetend is executed. The if-
condition tests whether
y
is even, and this test can be made by looking at the
rightmost bit of the binary representation of
y
. Since this bit is
1
, meaning
y
is
odd, the else-part is executed, which subtracts
1
from
y
, yielding
100
.
/**
Set
z
to
b^c
, given
c≥0 */
int
x= b;
int
y= c; z= 1;
// {
invariant:
z*x
y
= b
c
, 0 ≤ y ≤ c }
while
(y != 0) {
if
(y%2==0) {
x= x * x;
y= y / 2;
}
else
{
z= z * x;
y= y - 1;
/**
Set
z
to
b^c
, given
c≥0 */
int
y= c;
z= 1;
// {
invariant:
z*b
y
= b
c
, 0 ≤ y ≤ c }
while
(y != 0) {
z= z * b;
y= y - 1;
}
// {
postcondition: z =
b
c
}
}
}
// {
postcondition: z =
b
c
}
Fast
exponentiation algorithm
Figure 7.1a:
Slow
exponentiation algorithm
Figure 7.1b:
Search WWH ::
Custom Search