© 1987 by British Computer Society
Derivation of Sorting Algorithms from a Specification
Computing and Information Studies, Griffith University, Nathan, QLD 4111, Australia
Received 1 April 1986; revised 1 September 1986
It is important to be able to derive different algorithms that meet a particular specification. Transformations on a program specification provide a systematic means for such an endeavour. Different transformations on a specification can yield new and alternative forms of invariants. These invariants, in turn, can provide the framework for the derivation of a variety of algorithms by the use of weakest precondition techniques. To demonstrate these ideas a number of well-known sorting algorithms are shown to be derivable from a single original program specification.
The intelligent use of equivalent forms is the touchstone of logical insight (S. K. Langer).