The Deductive Synthesis of Imperative LISP Programs

Zohar Manna, Richard Waldinger

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 in cludes assignment and destructive list operations (rplaca and rplacd) .

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.