The Deductive Synthesis of Imperative LISP Programs
Abstract
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).
Cite
Text
Manna and Waldinger. "The Deductive Synthesis of Imperative LISP Programs." AAAI Conference on Artificial Intelligence, 1987.Markdown
[Manna and Waldinger. "The Deductive Synthesis of Imperative LISP Programs." AAAI Conference on Artificial Intelligence, 1987.](https://mlanthology.org/aaai/1987/manna1987aaai-deductive/)BibTeX
@inproceedings{manna1987aaai-deductive,
title = {{The Deductive Synthesis of Imperative LISP Programs}},
author = {Manna, Zohar and Waldinger, Richard J.},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {1987},
pages = {155-160},
url = {https://mlanthology.org/aaai/1987/manna1987aaai-deductive/}
}