Reasoning about Abstract State Machines: The WAM Case Study
-----------------------------------------------------------

Gerhard Schellhorn, Wolfgang Ahrendt

   This paper describes the first half of the formal verification of a
   Prolog compiler with the KIV ("Karlsruhe Interactive Verifier") system. Our
   work is based on [BR95], where an operational Prolog semantics is defined using
   the formalism of Gurevich Abstract State Machines, and then refined in
   several steps to the Warren Abstract Machine (WAM). We define a general
   translation of sequential Abstract State Machines to Dynamic Logic, which
   formalizes correctness of such refinement steps as a deduction problem. A proof
   technique for verification is presented, which corresponds to the informal use of
   proof maps. 6 of the 12 given refinement steps were verified. We found that the
   proof sketches given in [BR95] hide a lot of implicit assumptions. We report on
   our experiences in uncovering these assumptions incrementally during formal
   verification, and the support KIV offers for such `evolutionary' correctness
   proofs.