author  wenzelm 
Thu, 23 Feb 2012 19:34:48 +0100  
changeset 46622  3ccecb301d4e 
parent 46582  dcc312f22ee8 
child 55656  eb07b0acbebc 
permissions  rwrr 
10148  1 
header {* Using Hoare Logic *} 
2 

31758  3 
theory Hoare_Ex 
4 
imports Hoare 

5 
begin 

10148  6 

7 
subsection {* State spaces *} 

8 

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

10148  12 

13 
record vars = 

14 
I :: nat 

15 
M :: nat 

16 
N :: nat 

17 
S :: nat 

18 

37671  19 
text {* While all of our variables happen to have the same type, 
20 
nothing would prevent us from working with manysorted 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. *} 

10148  24 

25 

26 
subsection {* Basic examples *} 

27 

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

10148  31 

37671  32 
text {* Using the basic @{text assign} rule directly is a bit 
33 
cumbersome. *} 

10148  34 

37671  35 
lemma " .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." 
10148  36 
by (rule assign) 
37 

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

10148  42 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

43 
lemma " .{True}. \<acute>N := 10 .{\<acute>N = 10}." 
10148  44 
by hoare 
45 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

46 
lemma " .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." 
10148  47 
by hoare 
48 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

49 
lemma " .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." 
10148  50 
by hoare simp 
51 

10838  52 
lemma " .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}." 
10148  53 
by hoare 
54 

10838  55 
lemma " .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}." 
10148  56 
by hoare simp 
57 

10838  58 
lemma " .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}." 
10148  59 
by hoare 
60 

10838  61 
lemma " .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}." 
10148  62 
by hoare simp 
63 

64 
lemma 

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

10148  68 
by hoare simp 
69 

37671  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 
extralogical nature of record fields, we cannot formulate a theorem 

73 
relating record selectors and updates schematically. *} 

10148  74 

10838  75 
lemma " .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}." 
10148  76 
by hoare 
77 

10838  78 
lemma " .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}." 
10148  79 
oops 
80 

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 

85 

86 

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

10148  90 

10838  91 
lemma " .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." 
10148  92 
proof  
10838  93 
have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}." 
10148  94 
by auto 
10838  95 
also have " ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." 
10148  96 
by hoare 
97 
finally show ?thesis . 

98 
qed 

99 

10838  100 
lemma " .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." 
10148  101 
proof  
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
10838
diff
changeset

102 
have "!!m n::nat. m = n > m + 1 ~= n" 
10148  103 
 {* inclusion of assertions expressed in ``pure'' logic, *} 
104 
 {* without mentioning the state space *} 

105 
by simp 

10838  106 
also have " .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." 
10148  107 
by hoare 
108 
finally show ?thesis . 

109 
qed 

110 

10838  111 
lemma " .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." 
10148  112 
by hoare simp 
113 

114 

115 
subsection {* Multiplication by addition *} 

116 

37671  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 singlestep Hoare rules. *} 

10148  121 

122 
lemma 

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

10148  127 
proof  
128 
let " _ ?while _" = ?thesis 

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

10838  131 
have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto 
132 
also have " ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}." 

10148  133 
proof 
10838  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}." 

10148  136 
by auto 
10838  137 
also have " ... ?c .{\<acute>?inv}." by hoare 
138 
finally show " .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." . 

10148  139 
qed 
10838  140 
also have "... <= .{\<acute>S = a * b}." by auto 
10148  141 
finally show ?thesis . 
142 
qed 

143 

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

10148  148 

149 
lemma 

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

10148  155 
by hoare auto 
156 

157 

158 
subsection {* Summing natural numbers *} 

159 

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

10148  163 

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

15569  169 

10148  170 
theorem 
171 
" .{True}. 

10838  172 
\<acute>S := 0; \<acute>I := 1; 
173 
WHILE \<acute>I ~= n 

10148  174 
DO 
10838  175 
\<acute>S := \<acute>S + \<acute>I; 
176 
\<acute>I := \<acute>I + 1 

10148  177 
OD 
10838  178 
.{\<acute>S = (SUM j<n. j)}." 
10148  179 
(is " _ (_; ?while) _") 
180 
proof  

15049  181 
let ?sum = "\<lambda>k::nat. SUM j<k. j" 
182 
let ?inv = "\<lambda>s i::nat. s = ?sum i" 

10148  183 

10838  184 
have " .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." 
10148  185 
proof  
186 
have "True > 0 = ?sum 1" 

187 
by simp 

10838  188 
also have " .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." 
10148  189 
by hoare 
190 
finally show ?thesis . 

191 
qed 

10838  192 
also have " ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}." 
10148  193 
proof 
10838  194 
let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1" 
10148  195 
have "!!s i. ?inv s i & i ~= n > ?inv (s + i) (i + 1)" 
196 
by simp 

10838  197 
also have " .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}." 
10148  198 
by hoare 
10838  199 
finally show " .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." . 
10148  200 
qed 
201 
also have "!!s i. s = ?sum i & ~ i ~= n > s = ?sum n" 

202 
by simp 

203 
finally show ?thesis . 

204 
qed 

205 

37671  206 
text {* The next version uses the @{text hoare} method, while still 
207 
explaining the resulting proof obligations in an abstract, 

208 
structured manner. *} 

10148  209 

210 
theorem 

211 
" .{True}. 

10838  212 
\<acute>S := 0; \<acute>I := 1; 
213 
WHILE \<acute>I ~= n 

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

10148  215 
DO 
10838  216 
\<acute>S := \<acute>S + \<acute>I; 
217 
\<acute>I := \<acute>I + 1 

10148  218 
OD 
10838  219 
.{\<acute>S = (SUM j<n. j)}." 
10148  220 
proof  
15049  221 
let ?sum = "\<lambda>k::nat. SUM j<k. j" 
222 
let ?inv = "\<lambda>s i::nat. s = ?sum i" 

10148  223 

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" 

37671  229 
then show "?inv (s + i) (i + 1)" by simp 
10148  230 
next 
231 
fix s i assume "?inv s i & ~ i ~= n" 

37671  232 
then show "s = ?sum n" by simp 
10148  233 
qed 
234 
qed 

235 

37671  236 
text {* Certainly, this proof may be done fully automatic as well, 
237 
provided that the invariant is given beforehand. *} 

10148  238 

239 
theorem 

240 
" .{True}. 

10838  241 
\<acute>S := 0; \<acute>I := 1; 
242 
WHILE \<acute>I ~= n 

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

10148  244 
DO 
10838  245 
\<acute>S := \<acute>S + \<acute>I; 
246 
\<acute>I := \<acute>I + 1 

10148  247 
OD 
10838  248 
.{\<acute>S = (SUM j<n. j)}." 
10148  249 
by hoare auto 
250 

18193  251 

46622  252 
subsection {* Time *} 
13473  253 

46622  254 
text {* A simple embedding of time in Hoare logic: function @{text 
37671  255 
timeit} inserts an extra variable to keep track of the elapsed time. *} 
13473  256 

257 
record tstate = time :: nat 

258 

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

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

18193  263 
"timeit (Basic f) = (Basic f; Basic(\<lambda>s. s\<lparr>time := Suc (time s)\<rparr>))" 
37671  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)" 

13473  267 

268 
record tvars = tstate + 

269 
I :: nat 

270 
J :: nat 

271 

18193  272 
lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)" 
273 
by (induct n) simp_all 

13473  274 

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

277 
timeit ( 

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

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

280 
DO 

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

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

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

284 
DO \<acute>J := \<acute>J  1 OD; 

285 
\<acute>I := \<acute>I  1 

286 
OD 

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

18193  288 
apply simp 
289 
apply hoare 

290 
apply simp 

291 
apply clarsimp 

292 
apply clarsimp 

20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20272
diff
changeset

293 
apply arith 
18193  294 
prefer 2 
13473  295 
apply clarsimp 
18193  296 
apply (clarsimp simp: nat_distrib) 
297 
apply (frule lem) 

13473  298 
apply arith 
18193  299 
done 
13473  300 

301 
end 