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 reeursive 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.
sorting formal derivation loop invariant, automatic generation
SHI Haihe SHI Haipeng XUE Jinyun
Institute of Software, Chinese Academy of Sciences, Beijing 100080, China;Graduate University of Chi College of Software, Jiangxi Normal University, Nanchang 330022, China Institute of Software, Chinese Academy of Sciences, Beijing 100080, China;College of Computer Inform
国际会议
武汉
英文
311-316
2007-07-25（万方平台首次上网日期，不代表论文的发表时间）