@@ -21,31 +21,33 @@
|- 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
+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 prof. Example:
+side of an assignment in prog. Example:
The implementation hides reasoning in Hoare logic completely and provides a
-tactic hoare_tac for generating the verification conditions in ordinary
-logic:
+tactic hoare_tac for transforming a goal in Hoare logic into an
+equivalent list of verification conditions in HOL:
IMPORTANT:
@@ -53,18 +55,16 @@
does the right thing if it terminates, but not that it
terminates.
-
-
-
+The implementation loosely follows
+
Mike Gordon.
Mechanizing Programming Logics in Higher Order Logic.
-
-published as
-
+University of Cambridge, Computer Laboratory, TR 145, 1988.
+
+published as
+
Mike Gordon.
Mechanizing Programming Logics in Higher Order Logic.
-At the top level, it provides a tactic hoare_tac, which transforms a
-goal
-
-
-Note: Program variables are typed in the same way as HOL
-variables. Although you can write programs over arbitrary types, all
-program variables in a particular program must be of the same type!
+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.
|- 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 and postconditions
+value of x and is not a program variable. Pre/post conditions
can be arbitrary HOL formulae mentioning both program variables and normal
variables.
by(hoare_tac tac i);
applies the tactic to subgoal i and applies the parameter
-tac to all generated verification conditions. A typical call is
+tac (of type int -> tactic) to all generated
+verification conditions. A typical call is
by(hoare_tac Asm_full_simp_tac 1);
-which, given the example goal above, solves it completely.
+which, given the example goal above, solves it completely. For further
+examples see Examples.ML.
Notes on the implementation
+Notes on the implementation
-This directory contains a sugared shallow semantic embedding of Hoare logic
-for a while language. The implementation closely follows
-University of Cambridge, Computer Laboratory, TR 145, 1988.
In
@@ -73,21 +73,12 @@
edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989.
-{P} prog {Q}
-
-into a set of HOL-level verification conditions.
-
-
-The pre/post conditions can be arbitrary HOL formulae including program
-variables. The program text should only refer to program variables.
+The main differences: the state is modelled as a tuple as suggested in