Java Reference

In-Depth Information

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
!

See lesson

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:

Search WWH ::

Custom Search