1 |
|
2 header {* Using Hoare Logic *} |
|
3 |
|
4 theory HoareEx imports Hoare begin |
|
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 |
|
42 "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." |
|
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 |
|
52 lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}." |
|
53 by hoare |
|
54 |
|
55 lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." |
|
56 by hoare |
|
57 |
|
58 lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." |
|
59 by hoare simp |
|
60 |
|
61 lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}." |
|
62 by hoare |
|
63 |
|
64 lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}." |
|
65 by hoare simp |
|
66 |
|
67 lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}." |
|
68 by hoare |
|
69 |
|
70 lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}." |
|
71 by hoare simp |
|
72 |
|
73 lemma |
|
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}." |
|
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 |
|
86 lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}." |
|
87 by hoare |
|
88 |
|
89 lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}." |
|
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 |
|
104 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
|
105 proof - |
|
106 have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}." |
|
107 by auto |
|
108 also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
|
109 by hoare |
|
110 finally show ?thesis . |
|
111 qed |
|
112 |
|
113 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
|
114 proof - |
|
115 have "!!m n::nat. m = n --> m + 1 ~= n" |
|
116 -- {* inclusion of assertions expressed in ``pure'' logic, *} |
|
117 -- {* without mentioning the state space *} |
|
118 by simp |
|
119 also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
|
120 by hoare |
|
121 finally show ?thesis . |
|
122 qed |
|
123 |
|
124 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
|
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 |
|
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}." |
|
142 proof - |
|
143 let "|- _ ?while _" = ?thesis |
|
144 let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}." |
|
145 |
|
146 have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto |
|
147 also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}." |
|
148 proof |
|
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}." |
|
151 by auto |
|
152 also have "|- ... ?c .{\<acute>?inv}." by hoare |
|
153 finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." . |
|
154 qed |
|
155 also have "... <= .{\<acute>S = a * b}." by auto |
|
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 |
|
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}." |
|
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 |
|
191 declare atLeast0LessThan[symmetric,simp] |
|
192 |
|
193 theorem |
|
194 "|- .{True}. |
|
195 \<acute>S := 0; \<acute>I := 1; |
|
196 WHILE \<acute>I ~= n |
|
197 DO |
|
198 \<acute>S := \<acute>S + \<acute>I; |
|
199 \<acute>I := \<acute>I + 1 |
|
200 OD |
|
201 .{\<acute>S = (SUM j<n. j)}." |
|
202 (is "|- _ (_; ?while) _") |
|
203 proof - |
|
204 let ?sum = "\<lambda>k::nat. SUM j<k. j" |
|
205 let ?inv = "\<lambda>s i::nat. s = ?sum i" |
|
206 |
|
207 have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." |
|
208 proof - |
|
209 have "True --> 0 = ?sum 1" |
|
210 by simp |
|
211 also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." |
|
212 by hoare |
|
213 finally show ?thesis . |
|
214 qed |
|
215 also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}." |
|
216 proof |
|
217 let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1" |
|
218 have "!!s i. ?inv s i & i ~= n --> ?inv (s + i) (i + 1)" |
|
219 by simp |
|
220 also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}." |
|
221 by hoare |
|
222 finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." . |
|
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}. |
|
236 \<acute>S := 0; \<acute>I := 1; |
|
237 WHILE \<acute>I ~= n |
|
238 INV .{\<acute>S = (SUM j<\<acute>I. j)}. |
|
239 DO |
|
240 \<acute>S := \<acute>S + \<acute>I; |
|
241 \<acute>I := \<acute>I + 1 |
|
242 OD |
|
243 .{\<acute>S = (SUM j<n. j)}." |
|
244 proof - |
|
245 let ?sum = "\<lambda>k::nat. SUM j<k. j" |
|
246 let ?inv = "\<lambda>s i::nat. s = ?sum i" |
|
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}. |
|
267 \<acute>S := 0; \<acute>I := 1; |
|
268 WHILE \<acute>I ~= n |
|
269 INV .{\<acute>S = (SUM j<\<acute>I. j)}. |
|
270 DO |
|
271 \<acute>S := \<acute>S + \<acute>I; |
|
272 \<acute>I := \<acute>I + 1 |
|
273 OD |
|
274 .{\<acute>S = (SUM j<n. j)}." |
|
275 by hoare auto |
|
276 |
|
277 |
|
278 subsection{* Time *} |
|
279 |
|
280 text{* |
|
281 A simple embedding of time in Hoare logic: function @{text timeit} |
|
282 inserts an extra variable to keep track of the elapsed time. |
|
283 *} |
|
284 |
|
285 record tstate = time :: nat |
|
286 |
|
287 types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>" |
|
288 |
|
289 consts timeit :: "'a time com \<Rightarrow> 'a time com" |
|
290 primrec |
|
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)" |
|
295 |
|
296 record tvars = tstate + |
|
297 I :: nat |
|
298 J :: nat |
|
299 |
|
300 lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)" |
|
301 by (induct n) simp_all |
|
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}." |
|
315 apply simp |
|
316 apply hoare |
|
317 apply simp |
|
318 apply clarsimp |
|
319 apply clarsimp |
|
320 apply arith |
|
321 prefer 2 |
|
322 apply clarsimp |
|
323 apply (clarsimp simp: nat_distrib) |
|
324 apply (frule lem) |
|
325 apply arith |
|
326 done |
|
327 |
|
328 end |
|