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. A logic of total correctness is also provided and described below.

Total correctness

To prove termination, each WHILE-loop must be annotated with a variant: A variant is an expression with type nat, which may use program variables and normal variables.

A total-correctness goal has the form 

VARS x y ... [P] prog [Q]
enclosing the pre- and postcondition in square brackets.

Methods vcg_tc and vcg_tc_simp can be used to derive verification conditions.

From a total-correctness proof, a function can be extracted which for every input satisfying the precondition returns an output satisfying the postcondition.

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.