Symbolic Evaluation of LISP Functions with Side Effects for Verification
Proceedings of the Seventh International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 519-523.
Abstract
In this paper we present a symbolic evaluator of LISP functions. It can handle data-altering functions of the RPLACA type, i.e. functions that change one datastructure by replacing parts of it by other structures that will themselves not be changed further, at least not permanently. The state description language uses first-order predicate calculus. It is argued that symbolic evaluation in terms of this language, although theoretically adequate, is not feasible in general, since it may require extremely complicated specifications for real-life functions with side effects. Examples are given of the specifications needed to verify several versions of SUBSTAD, a non-copying SUBST.
@inproceedings{ijcai1981p97,
title = {Symbolic Evaluation of LISP Functions with Side Effects for Verification},
author = {de Champeaux, Dennis and de Bruin, Jos},
booktitle = {Proceedings of the Seventh International Joint Conference on
Artificial Intelligence, {IJCAI-81}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Roger C. Schank},
pages = {519--523},
year = {1981},
month = {8},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1981/97},
}
TY - CPAPER TI - Symbolic Evaluation of LISP Functions with Side Effects for Verification AU - de Champeaux, Dennis AU - de Bruin, Jos T2 - Proceedings of the Seventh International Joint Conference on Artificial Intelligence, IJCAI-81 PB - International Joint Conferences on Artificial Intelligence PY - 1981 SP - 519 EP - 523 UR - https://ijcai.org/proceedings/1981/97 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
