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

Search WWH ::

Custom Search