author | chaieb |
Mon, 11 Jun 2007 11:06:00 +0200 | |
changeset 23314 | 6894137e854a |
parent 21226 | a607ae87ee81 |
child 25706 | 45d090186bbe |
permissions | -rw-r--r-- |
10148 | 1 |
|
2 |
header {* Using Hoare Logic *} |
|
3 |
||
16417 | 4 |
theory HoareEx imports Hoare begin |
10148 | 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 |
|
21226
a607ae87ee81
field-update in records is generalised to take a function on the field
schirmer
parents:
20432
diff
changeset
|
42 |
"|- .{\<acute>(N_update (K_record (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 |
text {* |
|
184 |
The following proof is quite explicit in the individual steps taken, |
|
185 |
with the \name{hoare} method only applied locally to take care of |
|
186 |
assignment and sequential composition. Note that we express |
|
187 |
intermediate proof obligation in pure logic, without referring to the |
|
188 |
state space. |
|
189 |
*} |
|
190 |
||
15912 | 191 |
declare atLeast0LessThan[symmetric,simp] |
15569 | 192 |
|
10148 | 193 |
theorem |
194 |
"|- .{True}. |
|
10838 | 195 |
\<acute>S := 0; \<acute>I := 1; |
196 |
WHILE \<acute>I ~= n |
|
10148 | 197 |
DO |
10838 | 198 |
\<acute>S := \<acute>S + \<acute>I; |
199 |
\<acute>I := \<acute>I + 1 |
|
10148 | 200 |
OD |
10838 | 201 |
.{\<acute>S = (SUM j<n. j)}." |
10148 | 202 |
(is "|- _ (_; ?while) _") |
203 |
proof - |
|
15049 | 204 |
let ?sum = "\<lambda>k::nat. SUM j<k. j" |
205 |
let ?inv = "\<lambda>s i::nat. s = ?sum i" |
|
10148 | 206 |
|
10838 | 207 |
have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." |
10148 | 208 |
proof - |
209 |
have "True --> 0 = ?sum 1" |
|
210 |
by simp |
|
10838 | 211 |
also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." |
10148 | 212 |
by hoare |
213 |
finally show ?thesis . |
|
214 |
qed |
|
10838 | 215 |
also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}." |
10148 | 216 |
proof |
10838 | 217 |
let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1" |
10148 | 218 |
have "!!s i. ?inv s i & i ~= n --> ?inv (s + i) (i + 1)" |
219 |
by simp |
|
10838 | 220 |
also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}." |
10148 | 221 |
by hoare |
10838 | 222 |
finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." . |
10148 | 223 |
qed |
224 |
also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n" |
|
225 |
by simp |
|
226 |
finally show ?thesis . |
|
227 |
qed |
|
228 |
||
229 |
text {* |
|
230 |
The next version uses the \name{hoare} method, while still explaining |
|
231 |
the resulting proof obligations in an abstract, structured manner. |
|
232 |
*} |
|
233 |
||
234 |
theorem |
|
235 |
"|- .{True}. |
|
10838 | 236 |
\<acute>S := 0; \<acute>I := 1; |
237 |
WHILE \<acute>I ~= n |
|
238 |
INV .{\<acute>S = (SUM j<\<acute>I. j)}. |
|
10148 | 239 |
DO |
10838 | 240 |
\<acute>S := \<acute>S + \<acute>I; |
241 |
\<acute>I := \<acute>I + 1 |
|
10148 | 242 |
OD |
10838 | 243 |
.{\<acute>S = (SUM j<n. j)}." |
10148 | 244 |
proof - |
15049 | 245 |
let ?sum = "\<lambda>k::nat. SUM j<k. j" |
246 |
let ?inv = "\<lambda>s i::nat. s = ?sum i" |
|
10148 | 247 |
|
248 |
show ?thesis |
|
249 |
proof hoare |
|
250 |
show "?inv 0 1" by simp |
|
251 |
next |
|
252 |
fix s i assume "?inv s i & i ~= n" |
|
253 |
thus "?inv (s + i) (i + 1)" by simp |
|
254 |
next |
|
255 |
fix s i assume "?inv s i & ~ i ~= n" |
|
256 |
thus "s = ?sum n" by simp |
|
257 |
qed |
|
258 |
qed |
|
259 |
||
260 |
text {* |
|
261 |
Certainly, this proof may be done fully automatic as well, provided |
|
262 |
that the invariant is given beforehand. |
|
263 |
*} |
|
264 |
||
265 |
theorem |
|
266 |
"|- .{True}. |
|
10838 | 267 |
\<acute>S := 0; \<acute>I := 1; |
268 |
WHILE \<acute>I ~= n |
|
269 |
INV .{\<acute>S = (SUM j<\<acute>I. j)}. |
|
10148 | 270 |
DO |
10838 | 271 |
\<acute>S := \<acute>S + \<acute>I; |
272 |
\<acute>I := \<acute>I + 1 |
|
10148 | 273 |
OD |
10838 | 274 |
.{\<acute>S = (SUM j<n. j)}." |
10148 | 275 |
by hoare auto |
276 |
||
18193 | 277 |
|
278 |
subsection{* Time *} |
|
13473 | 279 |
|
280 |
text{* |
|
18193 | 281 |
A simple embedding of time in Hoare logic: function @{text timeit} |
282 |
inserts an extra variable to keep track of the elapsed time. |
|
13473 | 283 |
*} |
284 |
||
285 |
record tstate = time :: nat |
|
286 |
||
18193 | 287 |
types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>" |
13473 | 288 |
|
289 |
consts timeit :: "'a time com \<Rightarrow> 'a time com" |
|
290 |
primrec |
|
18193 | 291 |
"timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))" |
292 |
"timeit (c1; c2) = (timeit c1; timeit c2)" |
|
293 |
"timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)" |
|
294 |
"timeit (While b iv c) = While b iv (timeit c)" |
|
13473 | 295 |
|
296 |
record tvars = tstate + |
|
297 |
I :: nat |
|
298 |
J :: nat |
|
299 |
||
18193 | 300 |
lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)" |
301 |
by (induct n) simp_all |
|
13473 | 302 |
|
303 |
lemma "|- .{i = \<acute>I & \<acute>time = 0}. |
|
304 |
timeit( |
|
305 |
WHILE \<acute>I \<noteq> 0 |
|
306 |
INV .{2*\<acute>time + \<acute>I*\<acute>I + 5*\<acute>I = i*i + 5*i}. |
|
307 |
DO |
|
308 |
\<acute>J := \<acute>I; |
|
309 |
WHILE \<acute>J \<noteq> 0 |
|
310 |
INV .{0 < \<acute>I & 2*\<acute>time + \<acute>I*\<acute>I + 3*\<acute>I + 2*\<acute>J - 2 = i*i + 5*i}. |
|
311 |
DO \<acute>J := \<acute>J - 1 OD; |
|
312 |
\<acute>I := \<acute>I - 1 |
|
313 |
OD |
|
314 |
) .{2*\<acute>time = i*i + 5*i}." |
|
18193 | 315 |
apply simp |
316 |
apply hoare |
|
317 |
apply simp |
|
318 |
apply clarsimp |
|
319 |
apply clarsimp |
|
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20272
diff
changeset
|
320 |
apply arith |
18193 | 321 |
prefer 2 |
13473 | 322 |
apply clarsimp |
18193 | 323 |
apply (clarsimp simp: nat_distrib) |
324 |
apply (frule lem) |
|
13473 | 325 |
apply arith |
18193 | 326 |
done |
13473 | 327 |
|
328 |
end |