Abstract interpretation based on oldt resolution

Autor:	Tadashi Kanamori, Tadashi Kawamura
Rok vydání:	1993
Předmět:	Correctness LOOP (programming language) Logic Computer science Programming language Property (programming) Resolution (logic) Abstract interpretation computer.software_genre Domain (software engineering) Prolog computer Interpreter computer.programming_language
Zdroj:	The Journal of Logic Programming. 15:1-30
ISSN:	0743-1066
DOI:	10.1016/0743-1066(93)90011-5
Popis:	This paper presents a unified framework for analyzing Prolog programs. The framework is based on OLDT resolution, a top-down Prolog interpreter with memo-ization. A run-time property of Prolog goals can be analyzed by executing the goals using an interpreter that is obtained by abstracting OLDT resolution according to the property. The execution never enters a nonterminating computation loop when the domain on which the abstract interpreter works is finite, and it does not waste time working on goals irrelevant to the given top-level goals. In addition, the behavior of the abstract interpreter is very close to the way human programmers usually analyze the property in their minds. The correctness and termination of the abstract interpreter are discussed as well.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_dedup___::98535a8ab7d0c2c9dbd2030963488d7f https://doi.org/10.1016/0743-1066(93)90011-5 Zobrazit plný text záznamu