LANSKY@SRI-WARBUCKS.ARPA (Amy Lansky) (06/06/86)
DEDUCTIVE SYNTHESIS OF SORTING PROGRAMS
Jon Traugott (JCT@SAIL)
Stanford University
11:00 AM, MONDAY, June 9
SRI International, Building E, Room EJ228 (new conference room)
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 20 steps per procedure) 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.
VISITORS: Please arrive 5 minutes early so that you can be escorted up
from the E-building receptionist's desk. Thanks!