Affordable Access

Publisher Website

Deductive synthesis of sorting programs

Authors
Journal
Journal of Symbolic Computation
0747-7171
Publisher
Elsevier
Publication Date
Volume
7
Issue
6
Identifiers
DOI: 10.1016/s0747-7171(89)80040-9
Disciplines
  • Computer Science

Abstract

Using the deductive synthesis framework developed by Manna and Waldinger we have derived a wide variety of recursive sorting programs. These derivations represent the first application of the deductive framework to the derivation of nontrivial algorithms. While the programs given were derived manually, we ultimately hope that a computer implementation of the system (of which none currently exists) will find similar programs automatically. Our derivations are intended to suggest this possibility; the proofs are short in relation to program complexity (on the order of 40 steps per program) and individual derivation steps are uncontrived. We also present a new rule for the generation of auxiliary procedures, a common “eureka” step in program construction.

There are no comments yet on this publication. Be the first to share your thoughts.