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