Note that each WHILE-loop must be annotated with an invariant.
Within the context of theory\<^verbatim>\<open>Hoare\<close>, you can state goals of the form
@{verbatim [display] \<open>VARS x y ... {P} prog {Q}\<close>} where\<^verbatim>\<open>prog\<close> is a program in the above language, \<^verbatim>\<open>P\<close> is the precondition, \<^verbatim>\<open>Q\<close> the postcondition, and \<^verbatim>\<open>x y ...\<close> is the list of all \<^emph>\<open>program
variables\<close> in \<^verbatim>\<open>prog\<close>. The latter list must be nonempty and it must include
all variables that occur on the left-hand side of an assignment in\<^verbatim>\<open>prog\<close>.
Example:
@{verbatim [display] \<open>VARS x {x = a} x := x+1 {x = a+1}\<close>}
The (normal) variable \<^verbatim>\<open>a\<close> is merely used to record the initial value of \<^verbatim>\<open>x\<close> 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 \<^verbatim>\<open>vcg\<close> for transforming a goal in Hoare logic into an equivalent list
of verification conditions in HOL: \<^theory_text>\<open>apply vcg\<close>
If you want to simplify the resulting verification conditions at the same
time: \<^theory_text>\<open>apply vcg_simp\<close> which, given the example goal above, solves it
completely. For further examples see \<^file>\<open>Examples.thy\<close>.
\<^bold>\<open>IMPORTANT:\<close>
This is a logic of partial correctness. You can only prove that your program
does the right thing \<^emph>\<open>if\<close> it terminates, but not \<^emph>\<open>that\<close> it terminates. A
logic of total correctness isalso provided and described below. \<close>
subsection \<open>Total correctness\<close>
text\<open> To prove termination, each WHILE-loop must be annotated with a variant:
\<^item> \<^verbatim>\<open>WHILE _ INV {_} VAR {_} DO _ OD\<close>
A variant is an expression with type \<^verbatim>\<open>nat\<close>, which may use program variables and normal variables.
A total-correctness goal has the form \<^verbatim>\<open>VARS x y ... [P] prog [Q]\<close> enclosing
the pre- and postcondition in square brackets.
Methods \<^verbatim>\<open>vcg_tc\<close> and \<^verbatim>\<open>vcg_tc_simp\<close> 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. \<close>
subsection \<open>Notes on the implementation\<close>
text\<open>
The implementation loosely follows
Mike Gordon. \<^emph>\<open>Mechanizing Programming Logics in Higher Order Logic\<close>.
University of Cambridge, Computer Laboratory, TR 145, 1988.
published as
Mike Gordon. \<^emph>\<open>Mechanizing Programming Logics in Higher Order Logic\<close>. In \<^emph>\<open>Current Trends in Hardware Verification and Automated Theorem Proving\<close>,
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. \<^emph>\<open>Mechanizing Some Advanced Refinement Concepts\<close>. 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. \<close>
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
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 ist noch experimentell.
