CLAM specification for provably correct compilation of CLP( R ) programs
Egon Börger, Rosario F. Salamone · 1995
The paper extends the correctness proof in [4] for compilation of Prolog programs on the WAM to CLP(R) programs on the Constraint Logic Arithmetic Machine (CLAM [8, 10]). This serves to illustrate, through a complex case study, how the evolving algebra specification methodology allows to incorporate modularity and extendability principles in system design. 1 1 Introduction This paper extends, to the Constraint Logic Arithmetic Machine (CLAM) and CLP(R) programs, the mathematical analysis of the Warren Abstract Machine (WAM) for executing Prolog and the resulting correctness proof for a general compilation scheme of Prolog to the WAM given in [4]. Starting from an abstract CLP(R) model---which paraphrases the primary model for Prolog defined in [5]---we follow the stepwise refinement of Prolog models to the WAM model given in [4] and enrich both the specification and the correctness proofs by what is needed to cover CLP(R) constraints and their implementation in the CLAM. Use of Gurev...