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 vcgIf you want to simplify the resulting verification conditions at the same time:
apply vcg_simpwhich, 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.
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.