The Deductive Synthesis of Imperative LISP Programs

A framework is described for the automatic synthesis of imperative programs, which may alter data structures and produce destructive side effects as part of their intended behavior. A program meeting a given specification is extracted from the proof of a theorem in a variant of situational logic, in which the states of a computation are explicit objects. As an example, an in-place reverse program has been derived in an imperative LISP, which includes assignment and destructive list operations (rplacu and rplacd).

Authors

• Zohar Manna Richard Waldinger

Keywords

No keywords are indexed for this paper.