Java Reference

In-Depth Information

where it remains to determine expressions
E
,
F
,
G
, and
H
. We calculate
E
and
F
,

leaving
G
and
H
to the reader, using the technique given at the end of Sec. IV.4.

We assume
n
is even and greater than
0
, so
n = 2*k
for some
k
and
n/2 = k
, and

we massage
P
:

P

= <n = 2*k>

f(N) = a*f(2*k) + b*f(2*k + 1)

= <
Definition of
f>

f(N) = a*f(k) + b*(f(k) + f(k+1))

= <
Rearrange
>

f(N) = (a+b)*f(k) + b*f(k+1)

This formula has the form
[n,a,b \ n/2,a+b,b]P
, so we can take
E
to be
a+b

and
F
to be
b
. Hence, the assignment is
n,a,b= n/2,a+b,b;
. The assignment to

b
is not needed. In the same way, we develop the multiple assignment for the

else-part and end up with this program:

n= N; a= 1; b= 0;

{
invariant
P: f(N) = a*f(n) + b*f(n+1)
}

while
(n != 0) {

if
(n
is even
)

n, a= n/2, a+b;

else

n, b= n/2, a+b;

}

As Edsger W. Dijkstra, who first developed this algorithm
in this fashion
in

the 1970s and called it
fusc
, would have said, “Ain't it a beaut?”.