author | wenzelm |
Sat, 06 Oct 2001 00:02:46 +0200 | |
changeset 11704 | 3c50a2cd6f00 |
parent 11701 | 3d51fbf81c17 |
child 13473 | 194e8d2cbe0f |
permissions | -rw-r--r-- |
10148 | 1 |
|
2 |
header {* Using Hoare Logic *} |
|
3 |
||
4 |
theory HoareEx = Hoare: |
|
5 |
||
6 |
subsection {* State spaces *} |
|
7 |
||
8 |
text {* |
|
9 |
First of all we provide a store of program variables that |
|
10 |
occur in any of the programs considered later. Slightly unexpected |
|
11 |
things may happen when attempting to work with undeclared variables. |
|
12 |
*} |
|
13 |
||
14 |
record vars = |
|
15 |
I :: nat |
|
16 |
M :: nat |
|
17 |
N :: nat |
|
18 |
S :: nat |
|
19 |
||
20 |
text {* |
|
21 |
While all of our variables happen to have the same type, nothing |
|
22 |
would prevent us from working with many-sorted programs as well, or |
|
23 |
even polymorphic ones. Also note that Isabelle/HOL's extensible |
|
24 |
record types even provides simple means to extend the state space |
|
25 |
later. |
|
26 |
*} |
|
27 |
||
28 |
||
29 |
subsection {* Basic examples *} |
|
30 |
||
31 |
text {* |
|
32 |
We look at few trivialities involving assignment and sequential |
|
33 |
composition, in order to get an idea of how to work with our |
|
34 |
formulation of Hoare Logic. |
|
35 |
*} |
|
36 |
||
37 |
text {* |
|
38 |
Using the basic \name{assign} rule directly is a bit cumbersome. |
|
39 |
*} |
|
40 |
||
41 |
lemma |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
42 |
"|- .{\<acute>(N_update (2 * \<acute>N)) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." |
10148 | 43 |
by (rule assign) |
44 |
||
45 |
text {* |
|
46 |
Certainly we want the state modification already done, e.g.\ by |
|
47 |
simplification. The \name{hoare} method performs the basic state |
|
48 |
update for us; we may apply the Simplifier afterwards to achieve |
|
49 |
``obvious'' consequences as well. |
|
50 |
*} |
|
51 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
52 |
lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}." |
10148 | 53 |
by hoare |
54 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
55 |
lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." |
10148 | 56 |
by hoare |
57 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
58 |
lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." |
10148 | 59 |
by hoare simp |
60 |
||
10838 | 61 |
lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}." |
10148 | 62 |
by hoare |
63 |
||
10838 | 64 |
lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}." |
10148 | 65 |
by hoare simp |
66 |
||
10838 | 67 |
lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}." |
10148 | 68 |
by hoare |
69 |
||
10838 | 70 |
lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}." |
10148 | 71 |
by hoare simp |
72 |
||
73 |
lemma |
|
10838 | 74 |
"|- .{\<acute>M = a & \<acute>N = b}. |
75 |
\<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I |
|
76 |
.{\<acute>M = b & \<acute>N = a}." |
|
10148 | 77 |
by hoare simp |
78 |
||
79 |
text {* |
|
80 |
It is important to note that statements like the following one can |
|
81 |
only be proven for each individual program variable. Due to the |
|
82 |
extra-logical nature of record fields, we cannot formulate a theorem |
|
83 |
relating record selectors and updates schematically. |
|
84 |
*} |
|
85 |
||
10838 | 86 |
lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}." |
10148 | 87 |
by hoare |
88 |
||
10838 | 89 |
lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}." |
10148 | 90 |
oops |
91 |
||
92 |
lemma |
|
93 |
"Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}" |
|
94 |
-- {* same statement without concrete syntax *} |
|
95 |
oops |
|
96 |
||
97 |
||
98 |
text {* |
|
99 |
In the following assignments we make use of the consequence rule in |
|
100 |
order to achieve the intended precondition. Certainly, the |
|
101 |
\name{hoare} method is able to handle this case, too. |
|
102 |
*} |
|
103 |
||
10838 | 104 |
lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
10148 | 105 |
proof - |
10838 | 106 |
have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}." |
10148 | 107 |
by auto |
10838 | 108 |
also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
10148 | 109 |
by hoare |
110 |
finally show ?thesis . |
|
111 |
qed |
|
112 |
||
10838 | 113 |
lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
10148 | 114 |
proof - |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10838
diff
changeset
|
115 |
have "!!m n::nat. m = n --> m + 1 ~= n" |
10148 | 116 |
-- {* inclusion of assertions expressed in ``pure'' logic, *} |
117 |
-- {* without mentioning the state space *} |
|
118 |
by simp |
|
10838 | 119 |
also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
10148 | 120 |
by hoare |
121 |
finally show ?thesis . |
|
122 |
qed |
|
123 |
||
10838 | 124 |
lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
10148 | 125 |
by hoare simp |
126 |
||
127 |
||
128 |
subsection {* Multiplication by addition *} |
|
129 |
||
130 |
text {* |
|
131 |
We now do some basic examples of actual \texttt{WHILE} programs. |
|
132 |
This one is a loop for calculating the product of two natural |
|
133 |
numbers, by iterated addition. We first give detailed structured |
|
134 |
proof based on single-step Hoare rules. |
|
135 |
*} |
|
136 |
||
137 |
lemma |
|
10838 | 138 |
"|- .{\<acute>M = 0 & \<acute>S = 0}. |
139 |
WHILE \<acute>M ~= a |
|
140 |
DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD |
|
141 |
.{\<acute>S = a * b}." |
|
10148 | 142 |
proof - |
143 |
let "|- _ ?while _" = ?thesis |
|
10838 | 144 |
let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}." |
10148 | 145 |
|
10838 | 146 |
have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto |
147 |
also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}." |
|
10148 | 148 |
proof |
10838 | 149 |
let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1" |
150 |
have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}." |
|
10148 | 151 |
by auto |
10838 | 152 |
also have "|- ... ?c .{\<acute>?inv}." by hoare |
153 |
finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." . |
|
10148 | 154 |
qed |
10838 | 155 |
also have "... <= .{\<acute>S = a * b}." by auto |
10148 | 156 |
finally show ?thesis . |
157 |
qed |
|
158 |
||
159 |
text {* |
|
160 |
The subsequent version of the proof applies the \name{hoare} method |
|
161 |
to reduce the Hoare statement to a purely logical problem that can be |
|
162 |
solved fully automatically. Note that we have to specify the |
|
163 |
\texttt{WHILE} loop invariant in the original statement. |
|
164 |
*} |
|
165 |
||
166 |
lemma |
|
10838 | 167 |
"|- .{\<acute>M = 0 & \<acute>S = 0}. |
168 |
WHILE \<acute>M ~= a |
|
169 |
INV .{\<acute>S = \<acute>M * b}. |
|
170 |
DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD |
|
171 |
.{\<acute>S = a * b}." |
|
10148 | 172 |
by hoare auto |
173 |
||
174 |
||
175 |
subsection {* Summing natural numbers *} |
|
176 |
||
177 |
text {* |
|
178 |
We verify an imperative program to sum natural numbers up to a given |
|
179 |
limit. First some functional definition for proper specification of |
|
180 |
the problem. |
|
181 |
*} |
|
182 |
||
183 |
consts |
|
184 |
sum :: "(nat => nat) => nat => nat" |
|
185 |
primrec |
|
186 |
"sum f 0 = 0" |
|
187 |
"sum f (Suc n) = f n + sum f n" |
|
188 |
||
189 |
syntax |
|
190 |
"_sum" :: "idt => nat => nat => nat" |
|
191 |
("SUM _<_. _" [0, 0, 10] 10) |
|
192 |
translations |
|
193 |
"SUM j<k. b" == "sum (\<lambda>j. b) k" |
|
194 |
||
195 |
text {* |
|
196 |
The following proof is quite explicit in the individual steps taken, |
|
197 |
with the \name{hoare} method only applied locally to take care of |
|
198 |
assignment and sequential composition. Note that we express |
|
199 |
intermediate proof obligation in pure logic, without referring to the |
|
200 |
state space. |
|
201 |
*} |
|
202 |
||
203 |
theorem |
|
204 |
"|- .{True}. |
|
10838 | 205 |
\<acute>S := 0; \<acute>I := 1; |
206 |
WHILE \<acute>I ~= n |
|
10148 | 207 |
DO |
10838 | 208 |
\<acute>S := \<acute>S + \<acute>I; |
209 |
\<acute>I := \<acute>I + 1 |
|
10148 | 210 |
OD |
10838 | 211 |
.{\<acute>S = (SUM j<n. j)}." |
10148 | 212 |
(is "|- _ (_; ?while) _") |
213 |
proof - |
|
214 |
let ?sum = "\<lambda>k. SUM j<k. j" |
|
215 |
let ?inv = "\<lambda>s i. s = ?sum i" |
|
216 |
||
10838 | 217 |
have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." |
10148 | 218 |
proof - |
219 |
have "True --> 0 = ?sum 1" |
|
220 |
by simp |
|
10838 | 221 |
also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." |
10148 | 222 |
by hoare |
223 |
finally show ?thesis . |
|
224 |
qed |
|
10838 | 225 |
also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}." |
10148 | 226 |
proof |
10838 | 227 |
let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1" |
10148 | 228 |
have "!!s i. ?inv s i & i ~= n --> ?inv (s + i) (i + 1)" |
229 |
by simp |
|
10838 | 230 |
also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}." |
10148 | 231 |
by hoare |
10838 | 232 |
finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." . |
10148 | 233 |
qed |
234 |
also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n" |
|
235 |
by simp |
|
236 |
finally show ?thesis . |
|
237 |
qed |
|
238 |
||
239 |
text {* |
|
240 |
The next version uses the \name{hoare} method, while still explaining |
|
241 |
the resulting proof obligations in an abstract, structured manner. |
|
242 |
*} |
|
243 |
||
244 |
theorem |
|
245 |
"|- .{True}. |
|
10838 | 246 |
\<acute>S := 0; \<acute>I := 1; |
247 |
WHILE \<acute>I ~= n |
|
248 |
INV .{\<acute>S = (SUM j<\<acute>I. j)}. |
|
10148 | 249 |
DO |
10838 | 250 |
\<acute>S := \<acute>S + \<acute>I; |
251 |
\<acute>I := \<acute>I + 1 |
|
10148 | 252 |
OD |
10838 | 253 |
.{\<acute>S = (SUM j<n. j)}." |
10148 | 254 |
proof - |
255 |
let ?sum = "\<lambda>k. SUM j<k. j" |
|
256 |
let ?inv = "\<lambda>s i. s = ?sum i" |
|
257 |
||
258 |
show ?thesis |
|
259 |
proof hoare |
|
260 |
show "?inv 0 1" by simp |
|
261 |
next |
|
262 |
fix s i assume "?inv s i & i ~= n" |
|
263 |
thus "?inv (s + i) (i + 1)" by simp |
|
264 |
next |
|
265 |
fix s i assume "?inv s i & ~ i ~= n" |
|
266 |
thus "s = ?sum n" by simp |
|
267 |
qed |
|
268 |
qed |
|
269 |
||
270 |
text {* |
|
271 |
Certainly, this proof may be done fully automatic as well, provided |
|
272 |
that the invariant is given beforehand. |
|
273 |
*} |
|
274 |
||
275 |
theorem |
|
276 |
"|- .{True}. |
|
10838 | 277 |
\<acute>S := 0; \<acute>I := 1; |
278 |
WHILE \<acute>I ~= n |
|
279 |
INV .{\<acute>S = (SUM j<\<acute>I. j)}. |
|
10148 | 280 |
DO |
10838 | 281 |
\<acute>S := \<acute>S + \<acute>I; |
282 |
\<acute>I := \<acute>I + 1 |
|
10148 | 283 |
OD |
10838 | 284 |
.{\<acute>S = (SUM j<n. j)}." |
10148 | 285 |
by hoare auto |
286 |
||
287 |
end |