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

src/HOL/Isar_Examples/Hoare_Ex.thy

author | nipkow |

Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) | |

changeset 46372 | 6fa9cdb8b850 |

parent 41818 | 6d4c3ee8219d |

child 46582 | dcc312f22ee8 |

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

added "'a rel"

1 header {* Using Hoare Logic *}

3 theory Hoare_Ex

4 imports Hoare

5 begin

7 subsection {* State spaces *}

9 text {* 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. *}

13 record vars =

14 I :: nat

15 M :: nat

16 N :: nat

17 S :: nat

19 text {* While all of our variables happen to have the same type,

20 nothing would prevent us from working with many-sorted programs as

21 well, or even polymorphic ones. Also note that Isabelle/HOL's

22 extensible record types even provides simple means to extend the

23 state space later. *}

26 subsection {* Basic examples *}

28 text {* We look at few trivialities involving assignment and

29 sequential composition, in order to get an idea of how to work with

30 our formulation of Hoare Logic. *}

32 text {* Using the basic @{text assign} rule directly is a bit

33 cumbersome. *}

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

36 by (rule assign)

38 text {* Certainly we want the state modification already done, e.g.\

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

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

41 ``obvious'' consequences as well. *}

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

44 by hoare

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

47 by hoare

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

50 by hoare simp

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

53 by hoare

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

56 by hoare simp

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

59 by hoare

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

62 by hoare simp

64 lemma

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

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

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

68 by hoare simp

70 text {* It is important to note that statements like the following one

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

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

73 relating record selectors and updates schematically. *}

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

76 by hoare

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

79 oops

81 lemma

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

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

84 oops

87 text {* In the following assignments we make use of the consequence

88 rule in order to achieve the intended precondition. Certainly, the

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

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

92 proof -

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

94 by auto

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

96 by hoare

97 finally show ?thesis .

98 qed

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

101 proof -

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

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

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

105 by simp

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

107 by hoare

108 finally show ?thesis .

109 qed

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

112 by hoare simp

115 subsection {* Multiplication by addition *}

117 text {* We now do some basic examples of actual \texttt{WHILE}

118 programs. This one is a loop for calculating the product of two

119 natural numbers, by iterated addition. We first give detailed

120 structured proof based on single-step Hoare rules. *}

122 lemma

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

124 WHILE \<acute>M ~= a

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

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

127 proof -

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

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

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

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

133 proof

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

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

136 by auto

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

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

139 qed

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

141 finally show ?thesis .

142 qed

144 text {* The subsequent version of the proof applies the @{text hoare}

145 method to reduce the Hoare statement to a purely logical problem

146 that can be solved fully automatically. Note that we have to

147 specify the \texttt{WHILE} loop invariant in the original statement. *}

149 lemma

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

151 WHILE \<acute>M ~= a

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

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

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

155 by hoare auto

158 subsection {* Summing natural numbers *}

160 text {* We verify an imperative program to sum natural numbers up to a

161 given limit. First some functional definition for proper

162 specification of the problem. *}

164 text {* The following proof is quite explicit in the individual steps

165 taken, with the \name{hoare} method only applied locally to take

166 care of assignment and sequential composition. Note that we express

167 intermediate proof obligation in pure logic, without referring to

168 the state space. *}

170 theorem

171 "|- .{True}.

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

173 WHILE \<acute>I ~= n

174 DO

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

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

177 OD

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

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

180 proof -

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

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

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

185 proof -

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

187 by simp

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

189 by hoare

190 finally show ?thesis .

191 qed

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

193 proof

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

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

196 by simp

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

198 by hoare

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

200 qed

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

202 by simp

203 finally show ?thesis .

204 qed

206 text {* The next version uses the @{text hoare} method, while still

207 explaining the resulting proof obligations in an abstract,

208 structured manner. *}

210 theorem

211 "|- .{True}.

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

213 WHILE \<acute>I ~= n

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

215 DO

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

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

218 OD

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

220 proof -

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

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

224 show ?thesis

225 proof hoare

226 show "?inv 0 1" by simp

227 next

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

229 then show "?inv (s + i) (i + 1)" by simp

230 next

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

232 then show "s = ?sum n" by simp

233 qed

234 qed

236 text {* Certainly, this proof may be done fully automatic as well,

237 provided that the invariant is given beforehand. *}

239 theorem

240 "|- .{True}.

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

242 WHILE \<acute>I ~= n

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

244 DO

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

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

247 OD

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

249 by hoare auto

252 subsection{* Time *}

254 text{* A simple embedding of time in Hoare logic: function @{text

255 timeit} inserts an extra variable to keep track of the elapsed time. *}

257 record tstate = time :: nat

259 type_synonym 'a time = "\<lparr>time :: nat, \<dots> :: 'a\<rparr>"

261 primrec timeit :: "'a time com \<Rightarrow> 'a time com"

262 where

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

264 | "timeit (c1; c2) = (timeit c1; timeit c2)"

265 | "timeit (Cond b c1 c2) = Cond b (timeit c1) (timeit c2)"

266 | "timeit (While b iv c) = While b iv (timeit c)"

268 record tvars = tstate +

269 I :: nat

270 J :: nat

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

273 by (induct n) simp_all

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

276 timeit(

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

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

279 DO

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

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

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

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

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

285 OD

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

287 apply simp

288 apply hoare

289 apply simp

290 apply clarsimp

291 apply clarsimp

292 apply arith

293 prefer 2

294 apply clarsimp

295 apply (clarsimp simp: nat_distrib)

296 apply (frule lem)

297 apply arith

298 done

300 end