Formal derivation and automatic generation of sorting algorithms

Sorting has a broad range of application. For both practical and theoretical reasons, sorting is one of the most widely studied problems in algorithm design. The paper presents our new formal methods and techniques, through which the ideas behind QuickSort algorithm are revealed naturally from a common formal sorting specification, and then its loop invariant and nonrecursive algorithmic solution are produced mechanically, despite that developing the loop invariant of recursive problem is a difficult task. Furthermore, instead of fresh formal derivation, the other two sorting algorithms, Selection Sort and Bubble Sort, are easily achieved by applying different problem partition to QuickSort case. By means of tools their executable language programs can automatically be generated. The whole formal development process that starts from a high-level specification and results in provably correct sorting algorithmic programs, is mechanizable and unified, meanwhile provides the basis for the construction of a system for algorithm design from formal specifications.