The WAM - Definition and Compiler Correctness (CROSBI ID 28963)
Prilog u knjizi | izvorni znanstveni rad
Podaci o odgovornosti
Boerger, Egon ; Rosenzweig, Dean
engleski
The WAM - Definition and Compiler Correctness
This paper provides a mathematical analysis of the Warren Abstract Machine for executing Prolog and a proof of its correctness. Starting from an abstract Prolog model which is close to the programmer's intuition, we derive the WAM methodically by stepwise refinement of Prolog models, proving correctness and completeness for each refinement step. Along the way we explicitely formulate, as proof assumptions, a set of natural conditions for a c ompiler to be correct, thus making our proof applicable to a whole class of compilers. The proof method provides a rigorous mathematical framework for the study of Prolog compilation techniques. It can be applied in a natural way to extensions and variants of Prolog and related WAMs allowing for parallelism, constraint handling, types, functional components---in some cases it has in fact been successfully extended. Our exposition assumes only a general understanding of Prolog. We reach full mathematical rigour, without heavy methodological overhead, by using Gurevich's notion of evolving al gebras.
WAM, evolving algebras, compilation
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
404-x.
objavljeno
Podaci o knjizi
Logic Programming: Formal Methods and Practical Applications
Beierle, Chris ; Pluemer, Lutz
Amsterdam: North-Holland
1995.
0-444-82092-2