KIT | KIT-Bibliothek | Impressum
Open Access Logo
URN: urn:nbn:de:swb:90-AAA217960

Proving compiler correctness with evolving algebra specifications

Beckert, Bernhard; Haehnle, Reiner


The purpose of this note is to define a framework for proving
compiler correctness with evolving algebra (EA) specifications.
Although our specific domain is the verification of a Prolog-to-WAM
compiler, we think that our considerations are fairly general and
they should be useful in other areas as well.

First we define our general view of the semantics of a programming
language, of how semantics can be specified using EAs, and of
compiler correctness; then we describe how the correctness of a
compiler may be proven; and finally we point out the differences
to the approach of Egon Boerger and Dean Rosenzweig and to the
notion of correctness as commonly used in logic.

Zugehörige Institution(en) am KIT Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Jahr 1996
Sprache Englisch
Identifikator KITopen ID: 21796
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,4.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page