summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Hoare_Ex.thy

author | haftmann |

Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) | |

changeset 37659 | 14cabf5fa710 |

parent 33026 | 8f35633c4922 |

child 37671 | fa53d267dab3 |

permissions | -rw-r--r-- |

more speaking names

1 header {* Using Hoare Logic *}

3 theory Hoare_Ex

4 imports Hoare

5 begin

7 subsection {* State spaces *}

9 text {*

10 First of all we provide a store of program variables that

11 occur in any of the programs considered later. Slightly unexpected

12 things may happen when attempting to work with undeclared variables.

13 *}

15 record vars =

16 I :: nat

17 M :: nat

18 N :: nat

19 S :: nat

21 text {*

22 While all of our variables happen to have the same type, nothing

23 would prevent us from working with many-sorted programs as well, or

24 even polymorphic ones. Also note that Isabelle/HOL's extensible

25 record types even provides simple means to extend the state space

26 later.

27 *}

30 subsection {* Basic examples *}

32 text {*

33 We look at few trivialities involving assignment and sequential

34 composition, in order to get an idea of how to work with our

35 formulation of Hoare Logic.

36 *}

38 text {*

39 Using the basic \name{assign} rule directly is a bit cumbersome.

40 *}

42 lemma

43 "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."

44 by (rule assign)

46 text {*

47 Certainly we want the state modification already done, e.g.\ by

48 simplification. The \name{hoare} method performs the basic state

49 update for us; we may apply the Simplifier afterwards to achieve

50 ``obvious'' consequences as well.

51 *}

53 lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}."

54 by hoare

56 lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."

57 by hoare

59 lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}."

60 by hoare simp

62 lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."

63 by hoare

65 lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}."

66 by hoare simp

68 lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."

69 by hoare

71 lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}."

72 by hoare simp

74 lemma

75 "|- .{\<acute>M = a & \<acute>N = b}.

76 \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I

77 .{\<acute>M = b & \<acute>N = a}."

78 by hoare simp

80 text {*

81 It is important to note that statements like the following one can

82 only be proven for each individual program variable. Due to the

83 extra-logical nature of record fields, we cannot formulate a theorem

84 relating record selectors and updates schematically.

85 *}

87 lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}."

88 by hoare

90 lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}."

91 oops

93 lemma

94 "Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}"

95 -- {* same statement without concrete syntax *}

96 oops

99 text {*

100 In the following assignments we make use of the consequence rule in

101 order to achieve the intended precondition. Certainly, the

102 \name{hoare} method is able to handle this case, too.

103 *}

105 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."

106 proof -

107 have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}."

108 by auto

109 also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."

110 by hoare

111 finally show ?thesis .

112 qed

114 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."

115 proof -

116 have "!!m n::nat. m = n --> m + 1 ~= n"

117 -- {* inclusion of assertions expressed in ``pure'' logic, *}

118 -- {* without mentioning the state space *}

119 by simp

120 also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."

121 by hoare

122 finally show ?thesis .

123 qed

125 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}."

126 by hoare simp

129 subsection {* Multiplication by addition *}

131 text {*

132 We now do some basic examples of actual \texttt{WHILE} programs.

133 This one is a loop for calculating the product of two natural

134 numbers, by iterated addition. We first give detailed structured

135 proof based on single-step Hoare rules.

136 *}

138 lemma

139 "|- .{\<acute>M = 0 & \<acute>S = 0}.

140 WHILE \<acute>M ~= a

141 DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD

142 .{\<acute>S = a * b}."

143 proof -

144 let "|- _ ?while _" = ?thesis

145 let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}."

147 have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto

148 also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}."

149 proof

150 let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1"

151 have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}."

152 by auto

153 also have "|- ... ?c .{\<acute>?inv}." by hoare

154 finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." .

155 qed

156 also have "... <= .{\<acute>S = a * b}." by auto

157 finally show ?thesis .

158 qed

160 text {*

161 The subsequent version of the proof applies the \name{hoare} method

162 to reduce the Hoare statement to a purely logical problem that can be

163 solved fully automatically. Note that we have to specify the

164 \texttt{WHILE} loop invariant in the original statement.

165 *}

167 lemma

168 "|- .{\<acute>M = 0 & \<acute>S = 0}.

169 WHILE \<acute>M ~= a

170 INV .{\<acute>S = \<acute>M * b}.

171 DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD

172 .{\<acute>S = a * b}."

173 by hoare auto

176 subsection {* Summing natural numbers *}

178 text {*

179 We verify an imperative program to sum natural numbers up to a given

180 limit. First some functional definition for proper specification of

181 the problem.

182 *}

184 text {*

185 The following proof is quite explicit in the individual steps taken,

186 with the \name{hoare} method only applied locally to take care of

187 assignment and sequential composition. Note that we express

188 intermediate proof obligation in pure logic, without referring to the

189 state space.

190 *}

192 declare atLeast0LessThan[symmetric,simp]

194 theorem

195 "|- .{True}.

196 \<acute>S := 0; \<acute>I := 1;

197 WHILE \<acute>I ~= n

198 DO

199 \<acute>S := \<acute>S + \<acute>I;

200 \<acute>I := \<acute>I + 1

201 OD

202 .{\<acute>S = (SUM j<n. j)}."

203 (is "|- _ (_; ?while) _")

204 proof -

205 let ?sum = "\<lambda>k::nat. SUM j<k. j"

206 let ?inv = "\<lambda>s i::nat. s = ?sum i"

208 have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."

209 proof -

210 have "True --> 0 = ?sum 1"

211 by simp

212 also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}."

213 by hoare

214 finally show ?thesis .

215 qed

216 also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}."

217 proof

218 let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"

219 have "!!s i. ?inv s i & i ~= n --> ?inv (s + i) (i + 1)"

220 by simp

221 also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}."

222 by hoare

223 finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." .

224 qed

225 also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n"

226 by simp

227 finally show ?thesis .

228 qed

230 text {*

231 The next version uses the \name{hoare} method, while still explaining

232 the resulting proof obligations in an abstract, structured manner.

233 *}

235 theorem

236 "|- .{True}.

237 \<acute>S := 0; \<acute>I := 1;

238 WHILE \<acute>I ~= n

239 INV .{\<acute>S = (SUM j<\<acute>I. j)}.

240 DO

241 \<acute>S := \<acute>S + \<acute>I;

242 \<acute>I := \<acute>I + 1

243 OD

244 .{\<acute>S = (SUM j<n. j)}."

245 proof -

246 let ?sum = "\<lambda>k::nat. SUM j<k. j"

247 let ?inv = "\<lambda>s i::nat. s = ?sum i"

249 show ?thesis

250 proof hoare

251 show "?inv 0 1" by simp

252 next

253 fix s i assume "?inv s i & i ~= n"

254 thus "?inv (s + i) (i + 1)" by simp

255 next

256 fix s i assume "?inv s i & ~ i ~= n"

257 thus "s = ?sum n" by simp

258 qed

259 qed

261 text {*

262 Certainly, this proof may be done fully automatic as well, provided

263 that the invariant is given beforehand.

264 *}

266 theorem

267 "|- .{True}.

268 \<acute>S := 0; \<acute>I := 1;

269 WHILE \<acute>I ~= n

270 INV .{\<acute>S = (SUM j<\<acute>I. j)}.

271 DO

272 \<acute>S := \<acute>S + \<acute>I;

273 \<acute>I := \<acute>I + 1

274 OD

275 .{\<acute>S = (SUM j<n. j)}."

276 by hoare auto

279 subsection{* Time *}

281 text{*

282 A simple embedding of time in Hoare logic: function @{text timeit}

283 inserts an extra variable to keep track of the elapsed time.

284 *}

286 record tstate = time :: nat

288 types 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"

290 consts timeit :: "'a time com \<Rightarrow> 'a time com"

291 primrec

292 "timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))"

293 "timeit (c1; c2) = (timeit c1; timeit c2)"

294 "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"

295 "timeit (While b iv c) = While b iv (timeit c)"

297 record tvars = tstate +

298 I :: nat

299 J :: nat

301 lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)"

302 by (induct n) simp_all

304 lemma "|- .{i = \<acute>I & \<acute>time = 0}.

305 timeit(

306 WHILE \<acute>I \<noteq> 0

307 INV .{2*\<acute>time + \<acute>I*\<acute>I + 5*\<acute>I = i*i + 5*i}.

308 DO

309 \<acute>J := \<acute>I;

310 WHILE \<acute>J \<noteq> 0

311 INV .{0 < \<acute>I & 2*\<acute>time + \<acute>I*\<acute>I + 3*\<acute>I + 2*\<acute>J - 2 = i*i + 5*i}.

312 DO \<acute>J := \<acute>J - 1 OD;

313 \<acute>I := \<acute>I - 1

314 OD

315 ) .{2*\<acute>time = i*i + 5*i}."

316 apply simp

317 apply hoare

318 apply simp

319 apply clarsimp

320 apply clarsimp

321 apply arith

322 prefer 2

323 apply clarsimp

324 apply (clarsimp simp: nat_distrib)

325 apply (frule lem)

326 apply arith

327 done

329 end