Formal Construction of a Sorting Algorithm

Starting from a general specification of the sorting of a sequence, and through successive transformations using the Bird-Meertens formalism, we obtain an efficient algorithm that uses the insertion technique. Further transformations are done in order to obtain a version which works with only one sequence and an index into it, and therefore can be translated straightforwardly to an imperative version with an array: the Insertion Sort. We conclude that the formalism used provides an adequate framework for an unifying study of the various sorting algorithms, but that it would be useful to add techniques for dealing with linear arrays. Apartado Postal 89000, Caracas 1089-A -- Tel'efono: 906-3261 Fax: 906-3243 borges@usb.ve jravelo@usb.ve 1 Introduction Richard Bird and Lambert Meertens have developed a functional calculus for program construction ([Bir87]), the so called Bird-Meertens formalism, which has been the framework of many recent works in transformational programming. We wante..