A Case Study in Logic Program Verification: the Vanilla Metainterpreter.
Dino Pedreschi, Salvatore Ruggieri · 1995
We take the formal verification of the Vanilla metainterpreter as an excuse for explaining a proof method for reasoning about logic programs. The choice of a semantics suitable for program verification is discussed. We consider a variant of the least Herbrand model semantics which abstracts from ill-typed atoms and the underlying (first order) language, thus enhancing modularity and ease of specification. Then, proof outlines and proof obligations are introduced in a Hoare's logic style. In the resulting proof theory, triples of the form fPregPfPostg can be derived for a program P , which allow us to establish partial and total correctness. As a consequence of our results, the correctness of Vanilla is directly proved (once again.) Keywords: Verification, program development, metaprogramming, formal methods. 1 Introduction Logic programming (and Prolog) is advertised as a declarative language, in the sense that specifications, when written in an appropriate syntax, can be dir...