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

src/HOL/Isar_examples/HoareEx.thy

author | haftmann |

Mon Jan 30 08:20:56 2006 +0100 (2006-01-30) | |

changeset 18851 | 9502ce541f01 |

parent 18193 | 54419506df9e |

child 20272 | 0ca998e83447 |

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

adaptions to codegen_package

2 header {* Using Hoare Logic *}

4 theory HoareEx imports Hoare begin

6 subsection {* State spaces *}

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 *}

14 record vars =

15 I :: nat

16 M :: nat

17 N :: nat

18 S :: nat

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 *}

29 subsection {* Basic examples *}

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 *}

37 text {*

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

39 *}

41 lemma

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

43 by (rule assign)

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 *}

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

53 by hoare

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

56 by hoare

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

59 by hoare simp

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

62 by hoare

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

65 by hoare simp

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

68 by hoare

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

71 by hoare simp

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

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 *}

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

87 by hoare

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

90 oops

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

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 *}

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

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

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

125 by hoare simp

128 subsection {* Multiplication by addition *}

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 *}

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}."

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

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 *}

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

175 subsection {* Summing natural numbers *}

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 *}

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 *}

191 declare atLeast0LessThan[symmetric,simp]

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"

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

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 *}

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"

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

260 text {*

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

262 that the invariant is given beforehand.

263 *}

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

278 subsection{* Time *}

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 *}

285 record tstate = time :: nat

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

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)"

296 record tvars = tstate +

297 I :: nat

298 J :: nat

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

301 by (induct n) simp_all

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

328 end