Java Reference

In-Depth Information

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
}

Search WWH ::

Custom Search