EVA STAR Trefferanzeige

Volltext Volltext.pdf1.pdf (237 KB)
URN (für Zitat) http://nbn-resolving.org/urn:nbn:de:swb:90-AAA267961
Titel Verification of a Prolog compiler - first steps with KIV.
Autor Schellhorn, Gerhard
Ahrendt, Wolfgang
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,27.)
This paper describes the first steps of the formal verification of
a Prolog compiler with the KIV system. We build upon the mathematical
definitions given by Boerger and Rosenzweig in [BR95]. There an
operational semantics of Prolog is defined using the formalism of
Evolving Algebras, and then transformed in several systematic steps
to the Warren Abstract Machine (WAM). To verify these transformation
steps formally in KIV, a translation of deterministic Evolving
Algebras to Dynamic Logic is defined, which may also be of general
interest. With this translation, correctness of transformation steps
becomes a problem of program equivalence in Dynamic Logic. We define
a proof technique for verifying such problems, which corresponds to
the use of proof maps in Evolving Algebras. Although the transfor-
mation steps are small enough for a mathematical analysis, this is not
sufficient for a successful formal correctness proof. Such a proof
requires to explicitly state a lot of facts, which were only impli-
citly assumed in the analysis.
We will argue that these assumptions cannot be guessed in a first
proof attempt, but have to be filled in incrementally. We report on
our experience with this `evolutionary' verification process for the
first transformation step, and the support KIV offers to do such
incremental correctness proofs.