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?”.