1 <HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY> |
1 <HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY> |
2 |
2 |
3 <H2>Semantic Embedding of Hoare Logic</H2> |
3 <H2>Hoare Logic for a Simple WHILE Language</H2> |
|
4 |
|
5 <H1>The language and logic<H1> |
|
6 |
|
7 This directory contains an implementation of Hoare logic for a simple WHILE |
|
8 language. The are |
|
9 <UL> |
|
10 <LI> SKIP |
|
11 <LI> _ := _ |
|
12 <LI> _ ; _ |
|
13 <LI> <kbd>IF _ THEN _ ELSE _ FI<kbd> |
|
14 <LI> WHILE _ INV {_} DO _ OD |
|
15 </UL> |
|
16 Note that each WHILE-loop must be annotated with an invariant. |
|
17 <P> |
|
18 |
|
19 After loading theory Hoare, you can state goals of the form |
|
20 <PRE> |
|
21 |- VARS x y ... . {P} prog {Q} |
|
22 </PRE> |
|
23 where <kbd>prog</kbd> is a program in the above language, <kbd>P</kbd> is the |
|
24 precondition, <kbd>Q</kbd> the postcondition, and <kbd>x y ...<kbd> is the |
|
25 list of all <i>program variables</i> in <kbd>prog</kbd>. The latter list must |
|
26 be nonempty and it must include all variables that occur on the left-hand |
|
27 side of an assignment in <kbd>prof</kbd>. Example: |
|
28 <PRE> |
|
29 |- VARS x. {x = a} x := x+1 {x = a+1} |
|
30 </PRE> |
|
31 The (normal) variable <kbd>a</kbd> is merely used to record the initial |
|
32 value of <kbd>x</kbd> and is not a program variable. Pre and postconditions |
|
33 can be arbitrary HOL formulae mentioning both program variables and normal |
|
34 variables. |
|
35 <P> |
|
36 |
|
37 The implementation hides reasoning in Hoare logic completely and provides a |
|
38 tactic hoare_tac for generating the verification conditions in ordinary |
|
39 logic: |
|
40 <PRE> |
|
41 by(hoare_tac tac i); |
|
42 </PRE> |
|
43 applies the tactic to subgoal <kbd>i</kbd> and applies the parameter |
|
44 <kbd>tac</kbd> to all generated verification conditions. A typical call is |
|
45 <PRE> |
|
46 by(hoare_tac Asm_full_simp_tac 1); |
|
47 </PRE> |
|
48 which, given the example goal above, solves it completely. |
|
49 <P> |
|
50 |
|
51 IMPORTANT: |
|
52 This is a logic of partial correctness. You can only prove that your program |
|
53 does the right thing <i>if</i> it terminates, but not <i>that</i> it |
|
54 terminates. |
|
55 |
|
56 <H1>Notes on the implementation</H1> |
4 |
57 |
5 This directory contains a sugared shallow semantic embedding of Hoare logic |
58 This directory contains a sugared shallow semantic embedding of Hoare logic |
6 for a while language. The implementation closely follows<P> |
59 for a while language. The implementation closely follows<P> |
7 |
60 |
8 |
61 |