Verification of a Prolog compiler - first steps with KIV
Gerhard Schellhorn, Wolfgang Ahrendt · 1996
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.