author | wenzelm |
Mon, 11 Sep 2023 19:30:48 +0200 | |
changeset 78659 | b5f3d1051b13 |
parent 75916 | b6589c8ccadd |
permissions | -rw-r--r-- |
75916
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
1 |
theory README imports Main |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
2 |
begin |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
3 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
4 |
section \<open>Hoare Logic for a Simple WHILE Language\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
5 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
6 |
subsection \<open>Language and logic\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
7 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
8 |
text \<open> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
9 |
This directory contains an implementation of Hoare logic for a simple WHILE |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
10 |
language. The constructs are |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
11 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
12 |
\<^item> \<^verbatim>\<open>SKIP\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
13 |
\<^item> \<^verbatim>\<open>_ := _\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
14 |
\<^item> \<^verbatim>\<open>_ ; _\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
15 |
\<^item> \<^verbatim>\<open>IF _ THEN _ ELSE _ FI\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
16 |
\<^item> \<^verbatim>\<open>WHILE _ INV {_} DO _ OD\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
17 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
18 |
Note that each WHILE-loop must be annotated with an invariant. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
19 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
20 |
Within the context of theory \<^verbatim>\<open>Hoare\<close>, you can state goals of the form |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
21 |
@{verbatim [display] \<open>VARS x y ... {P} prog {Q}\<close>} |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
22 |
where \<^verbatim>\<open>prog\<close> is a program in the above language, \<^verbatim>\<open>P\<close> is the precondition, |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
23 |
\<^verbatim>\<open>Q\<close> the postcondition, and \<^verbatim>\<open>x y ...\<close> is the list of all \<^emph>\<open>program |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
24 |
variables\<close> in \<^verbatim>\<open>prog\<close>. The latter list must be nonempty and it must include |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
25 |
all variables that occur on the left-hand side of an assignment in \<^verbatim>\<open>prog\<close>. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
26 |
Example: |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
27 |
@{verbatim [display] \<open>VARS x {x = a} x := x+1 {x = a+1}\<close>} |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
28 |
The (normal) variable \<^verbatim>\<open>a\<close> is merely used to record the initial value of |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
29 |
\<^verbatim>\<open>x\<close> and is not a program variable. Pre/post conditions can be arbitrary HOL |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
30 |
formulae mentioning both program variables and normal variables. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
31 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
32 |
The implementation hides reasoning in Hoare logic completely and provides a |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
33 |
method \<^verbatim>\<open>vcg\<close> for transforming a goal in Hoare logic into an equivalent list |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
34 |
of verification conditions in HOL: \<^theory_text>\<open>apply vcg\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
35 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
36 |
If you want to simplify the resulting verification conditions at the same |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
37 |
time: \<^theory_text>\<open>apply vcg_simp\<close> which, given the example goal above, solves it |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
38 |
completely. For further examples see \<^file>\<open>Examples.thy\<close>. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
39 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
40 |
\<^bold>\<open>IMPORTANT:\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
41 |
This is a logic of partial correctness. You can only prove that your program |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
42 |
does the right thing \<^emph>\<open>if\<close> it terminates, but not \<^emph>\<open>that\<close> it terminates. A |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
43 |
logic of total correctness is also provided and described below. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
44 |
\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
45 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
46 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
47 |
subsection \<open>Total correctness\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
48 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
49 |
text \<open> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
50 |
To prove termination, each WHILE-loop must be annotated with a variant: |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
51 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
52 |
\<^item> \<^verbatim>\<open>WHILE _ INV {_} VAR {_} DO _ OD\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
53 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
54 |
A variant is an expression with type \<^verbatim>\<open>nat\<close>, which may use program variables |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
55 |
and normal variables. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
56 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
57 |
A total-correctness goal has the form \<^verbatim>\<open>VARS x y ... [P] prog [Q]\<close> enclosing |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
58 |
the pre- and postcondition in square brackets. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
59 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
60 |
Methods \<^verbatim>\<open>vcg_tc\<close> and \<^verbatim>\<open>vcg_tc_simp\<close> can be used to derive verification |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
61 |
conditions. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
62 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
63 |
From a total-correctness proof, a function can be extracted which for every |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
64 |
input satisfying the precondition returns an output satisfying the |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
65 |
postcondition. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
66 |
\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
67 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
68 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
69 |
subsection \<open>Notes on the implementation\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
70 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
71 |
text \<open> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
72 |
The implementation loosely follows |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
73 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
74 |
Mike Gordon. \<^emph>\<open>Mechanizing Programming Logics in Higher Order Logic\<close>. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
75 |
University of Cambridge, Computer Laboratory, TR 145, 1988. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
76 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
77 |
published as |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
78 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
79 |
Mike Gordon. \<^emph>\<open>Mechanizing Programming Logics in Higher Order Logic\<close>. In |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
80 |
\<^emph>\<open>Current Trends in Hardware Verification and Automated Theorem Proving\<close>, |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
81 |
edited by G. Birtwistle and P.A. Subrahmanyam, Springer-Verlag, 1989. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
82 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
83 |
The main differences: the state is modelled as a tuple as suggested in |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
84 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
85 |
J. von Wright and J. Hekanaho and P. Luostarinen and T. Langbacka. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
86 |
\<^emph>\<open>Mechanizing Some Advanced Refinement Concepts\<close>. Formal Methods in System |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
87 |
Design, 3, 1993, 49-81. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
88 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
89 |
and the embeding is deep, i.e. there is a concrete datatype of programs. The |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
90 |
latter is not really necessary. |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
91 |
\<close> |
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
92 |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
93 |
end |