Java Reference

In-Depth Information

IV.5.2

Developing the repetend

The repetend of a while-loop has to do two things: make progress toward termi-

nation and keep the invariant true. Suppose we look at maintaining the invariant

for insight into the development of the repetend. All we can write is:

{
P && B
} skip {
P
}

because
skip
is the simplest way to maintain
P
, and there is little to suggest

doing something else.

Thus, when beginning development of the repetend, we should first see how

to make progress toward termination. Suppose making progress is done by incre-

menting
k
. The annotated repetend will be:

{
P and B
}
S; k= k+1;
{
P
}

where statement
S
is to be determined. Using the assignment statement axiom,

insert the precondition of the increment:

{
P and B
}
S;
{
[k\k+1]P
}
k= k+1;
{
P
}

This means that S has to satisfy the specification

{
P and B
}
S;
{
[k\k+1]P
}

and we can now begin to develop
S
to satisfy it.

This is top-down programming, or stepwise refinement, at its best. We de-

cide how to make progress; we
calculate
the specification of statement
S
that is

required to maintain the invariant, and we develop
S
to satisfy its specification.

Here is an example. Suppose invariant
P
is:

P:
the squares of
h..k-1
have been printed

and progress is to be made using
k= k+1;
. Then S has to satisfy:

{
the squares of
h..k-1
have been printed
and B
}

S;

{
the squares of
h..k
have been printed
}

and
S
is obviously
System.out.println(k*k);
.

Suppose the squares are being printed in reverse order, so that progress is

made by decreasing
h
. Then the annotated sequence is:

{
P and B
}
S;
{
[h\h-1]P
}
h= h-1;
{
P
}

so S has to satisfy:

{
the squares of
h..k-1
have been printed
and B
}

S;

{
the squares of
h-1..k-1
have been printed
}

So, statement
S
has to print
(h-1)*(h-1)
.

Search WWH ::

Custom Search