Hoare Logic for a Simple WHILE Language

Language and logic

This directory contains an implementation of Hoare logic for a simple WHILE language. The constructs are Note that each WHILE-loop must be annotated with an invariant.

After loading theory Hoare, you can state goals of the form

VARS x y ... {P} prog {Q}
where prog is a program in the above language, P is the precondition, Q the postcondition, and x y ... is the list of all program variables in prog. The latter list must be nonempty and it must include all variables that occur on the left-hand side of an assignment in prog. Example:
VARS x {x = a} x := x+1 {x = a+1}
The (normal) variable a is merely used to record the initial value of x and is not a program variable. Pre/post conditions can be arbitrary HOL formulae mentioning both program variables and normal variables.

The implementation hides reasoning in Hoare logic completely and provides a method vcg for transforming a goal in Hoare logic into an equivalent list of verification conditions in HOL:

apply vcg
If you want to simplify the resulting verification conditions at the same time:
apply vcg_simp
which, given the example goal above, solves it completely. For further examples see Examples.

IMPORTANT: This is a logic of partial correctness. You can only prove that your program does the right thing if it terminates, but not that it terminates.

Notes on the implementation

The implementation loosely follows

Mike Gordon. Mechanizing Programming Logics in Higher Order Logic.
University of Cambridge, Computer Laboratory, TR 145, 1988.

published as

Mike Gordon. Mechanizing Programming Logics in Higher Order Logic.
In Current Trends in Hardware Verification and Automated Theorem Proving ,
edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.

The main differences: the state is modelled as a tuple as suggested in

J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka. Mechanizing Some Advanced Refinement Concepts. Formal Methods in System Design, 3, 1993, 49-81.

and the embeding is deep, i.e. there is a concrete datatype of programs. The latter is not really necessary.