Symbolic Evaluation of LISP Functions with Side Effects for Verification
Abstract
In t h i s paper we present a symbolic evaluator of LISP func t i ons. I t can handle d a t a- a l t e r i n g funct ions of the RPLACA type, i. e. funct ions that change one datas t ruc ture by rep lac ing par ts of i t by other s t ruc tu res that w i l l themselves not be changed f u r t h e r, at leas t not permanently. The s ta te desc r ip t i on language uses f i r s t- o r d e r predicate ca l cu lus. I t i s argued tha t symbolic eva luat ion in terms of t h i s language, although
Cite
Text
de Champeaux and de Bruin. "Symbolic Evaluation of LISP Functions with Side Effects for Verification." International Joint Conference on Artificial Intelligence, 1981.Markdown
[de Champeaux and de Bruin. "Symbolic Evaluation of LISP Functions with Side Effects for Verification." International Joint Conference on Artificial Intelligence, 1981.](https://mlanthology.org/ijcai/1981/dechampeaux1981ijcai-symbolic/)BibTeX
@inproceedings{dechampeaux1981ijcai-symbolic,
title = {{Symbolic Evaluation of LISP Functions with Side Effects for Verification}},
author = {de Champeaux, Dennis and de Bruin, Jos},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1981},
pages = {519-524},
url = {https://mlanthology.org/ijcai/1981/dechampeaux1981ijcai-symbolic/}
}