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

src/HOL/Isar_examples/HoareEx.thy

author | oheimb |

Wed Jan 31 10:15:55 2001 +0100 (2001-01-31) | |

changeset 11008 | f7333f055ef6 |

parent 10838 | 9423817dee84 |

child 11701 | 3d51fbf81c17 |

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

improved theory reference in comment

2 header {* Using Hoare Logic *}

4 theory HoareEx = Hoare:

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. 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 consts

184 sum :: "(nat => nat) => nat => nat"

185 primrec

186 "sum f 0 = 0"

187 "sum f (Suc n) = f n + sum f n"

189 syntax

190 "_sum" :: "idt => nat => nat => nat"

191 ("SUM _<_. _" [0, 0, 10] 10)

192 translations

193 "SUM j<k. b" == "sum (\<lambda>j. b) k"

195 text {*

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

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

198 assignment and sequential composition. Note that we express

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

200 state space.

201 *}

203 theorem

204 "|- .{True}.

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

206 WHILE \<acute>I ~= n

207 DO

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

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

210 OD

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

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

213 proof -

214 let ?sum = "\<lambda>k. SUM j<k. j"

215 let ?inv = "\<lambda>s i. s = ?sum i"

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

218 proof -

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

220 by simp

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

222 by hoare

223 finally show ?thesis .

224 qed

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

226 proof

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

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

229 by simp

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

231 by hoare

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

233 qed

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

235 by simp

236 finally show ?thesis .

237 qed

239 text {*

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

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

242 *}

244 theorem

245 "|- .{True}.

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

247 WHILE \<acute>I ~= n

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

249 DO

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

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

252 OD

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

254 proof -

255 let ?sum = "\<lambda>k. SUM j<k. j"

256 let ?inv = "\<lambda>s i. s = ?sum i"

258 show ?thesis

259 proof hoare

260 show "?inv 0 1" by simp

261 next

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

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

264 next

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

266 thus "s = ?sum n" by simp

267 qed

268 qed

270 text {*

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

272 that the invariant is given beforehand.

273 *}

275 theorem

276 "|- .{True}.

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

278 WHILE \<acute>I ~= n

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

280 DO

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

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

283 OD

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

285 by hoare auto

287 end