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.

Statistics

Seen <100 times
0 Comments

More articles like this

Deductive and inductive synthesis of equational pr...

on Journal of Symbolic Computatio... Jan 01, 1993

A three-valued semantics for deductive databases a...

on Journal of Computer and System... Jan 01, 1994
More articles like this..