Derivation of sorting algorithms from a specification

Abstract

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). © 1987 The British Computer Society.