Note that each WHILE-loop must be annotated with an invariant.
Within the context of theory ▩‹Hoare›, you can state goals of the form
@{verbatim [display] ‹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:
@{verbatim [display] ‹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.thy›.
\‹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. ›
subsection‹Total correctness›
text‹
To prove termination, each WHILE-loop must be annotated with a variant:
▪▩‹WHILE _ INV {_} VAR {_} DO _ OD›
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. ›
subsection‹Notes on the implementation›
text‹
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. ›
end
Messung V0.5 in Prozent
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet am 2026-06-30)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
