EVA STAR Trefferanzeige

Volltext Volltext.pdf1.pdf (64 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-AAA217960
Titel Proving compiler correctness with evolving algebra specifications.
Autor Beckert, Bernhard
Haehnle, Reiner
Institution Fakultät für Informatik (INFORMATIK)
Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Dokumenttyp Buch
Jahr 1996
Erscheinungsvermerk Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,4.)
Abstract
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.