Correctness of programs - Multimedia Introduction to Programming Using Java - page 511

IV.6 A neat example: fusc

Consider a function f defined as follows —e.g. f(13) is 5 .

f(0) = 0
f(1) = 1
f(2*n) = f(n) (for n > 0)
f(2*n+1) = f(n) + f(n+1) (for n > 0)
We want a program segment S that, given N≥0 , calculates f(N) . One idea
would be to assign N to a fresh variable n and then repeatedly decrease n , main-
taining some invariant, until n is 0 or 1 . The first, naive, invariant would then be:

f(N) = f(n)
Indeed, if n is even, we can divide n by 2 and the invariant is maintained (since
f(2n) = f(n) . But if n is odd, there is no way to decrease n and keep this invari-
ant true. The invariant is too simple.
Where do we look for inspiration in developing the invariant? The only pos-
sible place is the definition of f . Even a postcondition like f(N) = b (meaning b
contains the answer) would not help. In Sec. IV.4, in developing a program seg-
ment to calculate max(x, y) , we also had to turn to the definition of max . Here,
it is the same thing: a definition provides the inspiration.
Notice that the right sides of two recursive formulas for f :

f(2*n) = f(n)
f(2*n+1) = f(n) + f(n+1)
are linear combinations of f(n) and f(n+1) :

f(2*n) = 1*f(n) + 0*f(n+1)
f(2*n+1) = 1*f(n) + 1*f(n+1)
and this inspires us to try an invariant in which the righthand side is a (more gen-
eral) linear combination of f(n) and f(n+1) :

P: f(N) = a*f(n) + b*f(n+1)
Now, we write the loop, hoping that we can make progress by halving n at
each iteration —but we assume we would need two cases, depending on whether
n is even or odd. We have skipped all the obvious steps of this development.

{ N>=0 }
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, b= n/2, E, F;
else n, a, b= n/2, G, H;

}
{ f(N) = b }