The deductive synthesis of imperative LISP programs
Zohar Manna, Richard J. Waldinger · National Conference on Artificial Intelligence · 1987
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 (rplaca and rplacd).