Java Reference
In-Depth Information
Dealing with pictures of arrays
Most algorithms that manipulate arrays require loops of some sort, and some
people prefer writing the pre- and post-conditions —and hence the invariant—
using array pictures. In many cases, the invariant can be seen to be a generaliza-
tion of both the pre- and the post-condition.
Here is an example. Below, we specify a sorting algorithm:
h k
?
Precondition:
b
h k
sorted
Postcondition:
b
Invariant
P
is a generalization of the precondition, so
P
, drawn as a picture, needs
a segment labeled “?”.
P
is also a generalization of the postcondition, so it needs
a segment labeled “sorted”. Thus, we use one of the following two alternatives
as the invariant. The first results in a loop that sorts from beginning to end; the
second, from end to beginning. (Of course, we have to label the boundary
between the two segments.):
h k
sorted ?
invariant P:
b
or
h k
? sorted
invariant P:
b
This business of developing the invariant as a picture that generalizes both
the pre- and the post-condition works quite well. Often it allows one to analyze
different algorithms for the same problem —the algorithms being expressed as
invariants— without writing a line of code.
Discussion
The three methods of developing an invariant work well in many cases.
Sometimes, they are only the start of the development of a full invariant in that
a simple but inefficient loop is developed from the invariant. Then, one may have
to strengthen the invariant (put more information in it) to remove the inefficien-
cies. But that topic is beyond the scope of this appendix (although it is a neat ,
useful idea).
Do not expect the methods discussed above to work in all cases. Sometimes,
an additional idea is needed, which is not easily seen. Sometimes, the formal def-
inition of whatever is being manipulated will provide insight into possible invari-
ants.
Search WWH ::
Custom Search