Proceedings:
Book One
Volume
Issue:
Proceedings of the AAAI Conference on Artificial Intelligence, 6
Track:
Automated Reasoning
Downloads:
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 in cludes assignment and destructive list operations (rplaca and rplacd) .
AAAI
Proceedings of the AAAI Conference on Artificial Intelligence, 6