-|- VARS x y ... {P} prog {Q}
+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
@@ -37,7 +37,7 @@
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}
+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
@@ -46,19 +46,18 @@
The implementation hides reasoning in Hoare logic completely and provides a -tactic hoare_tac for transforming a goal in Hoare logic into an +method vcg for transforming a goal in Hoare logic into an equivalent list of verification conditions in HOL:
-by(hoare_tac tac i); +apply vcg-applies the tactic to subgoal i and applies the parameter -tac (of type int -> tactic) to all generated -verification conditions. A typical call is +If you want to simplify the resulting verification conditions at the same +time:
-by(hoare_tac Asm_full_simp_tac 1); +apply vcg_simpwhich, given the example goal above, solves it completely. For further -examples see Examples.ML. +examples see Examples.
IMPORTANT: