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