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 ... mehr

Zugehörige Institution(en) am KIT |
Institut für Logik, Komplexität und Deduktionssysteme (ILKD) |

Publikationstyp |
Buch |

Jahr |
1996 |

Sprache |
Englisch |

Identifikator |
KITopen ID: 26796 |

Erscheinungsvermerk |
Karlsruhe 1996. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1996,27.) |

KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page