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