14 chains to HOL lists. This is merely axiomatized by Bornat. |
14 chains to HOL lists. This is merely axiomatized by Bornat. |
15 *) |
15 *) |
16 |
16 |
17 theory Pointers = Hoare: |
17 theory Pointers = Hoare: |
18 |
18 |
19 (* field access and update *) |
19 section "Syntactic sugar" |
|
20 |
|
21 types 'a ref = "'a option" |
|
22 |
|
23 syntax Null :: "'a ref" |
|
24 Ref :: "'a \<Rightarrow> 'a ref" |
|
25 addr :: "'a ref \<Rightarrow> 'a" |
|
26 translations |
|
27 "Null" => "None" |
|
28 "Ref" => "Some" |
|
29 "addr" => "the" |
|
30 |
|
31 text "Field access and update:" |
|
32 |
20 syntax |
33 syntax |
21 "@faccess" :: "'a option => ('a \<Rightarrow> 'v option) => 'v" |
34 "@refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" |
22 ("_^:_" [65,1000] 65) |
35 ("_/'((_ \<rightarrow> _)')" [1000,0] 900) |
23 "@fassign" :: "'p option => id => 'v => 's com" |
36 "@fassign" :: "'a ref => id => 'v => 's com" |
24 ("(2_^._ :=/ _)" [70,1000,65] 61) |
37 ("(2_^._ :=/ _)" [70,1000,65] 61) |
|
38 "@faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v" |
|
39 ("_^._" [65,1000] 65) |
25 translations |
40 translations |
26 "p^:f" == "f(the p)" |
41 "f(r \<rightarrow> v)" == "f(the r := v)" |
27 "p^.f := e" => "f := fun_upd f (the p) e" |
42 "p^.f := e" => "f := f(p \<rightarrow> e)" |
28 |
43 "p^.f" == "f(the p)" |
29 |
44 |
30 text{* An example due to Suzuki: *} |
45 |
|
46 text "An example due to Suzuki:" |
31 |
47 |
32 lemma "|- VARS v n. |
48 lemma "|- VARS v n. |
33 {w = Some w0 & x = Some x0 & y = Some y0 & z = Some z0 & |
49 {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 & |
34 distinct[w0,x0,y0,z0]} |
50 distinct[w0,x0,y0,z0]} |
35 w^.v := (1::int); w^.n := x; |
51 w^.v := (1::int); w^.n := x; |
36 x^.v := 2; x^.n := y; |
52 x^.v := 2; x^.n := y; |
37 y^.v := 3; y^.n := z; |
53 y^.v := 3; y^.n := z; |
38 z^.v := 4; x^.n := z |
54 z^.v := 4; x^.n := z |
39 {w^:n^:n^:v = 4}" |
55 {w^.n^.n^.v = 4}" |
40 by vcg_simp |
56 by vcg_simp |
41 |
57 |
42 |
58 |
43 section"The heap" |
59 section "The heap" |
44 |
60 |
45 subsection"Paths in the heap" |
61 subsection "Paths in the heap" |
46 |
62 |
47 consts |
63 consts |
48 path :: "('a \<leadsto> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> 'a option \<Rightarrow> bool" |
64 path :: "('a \<leadsto> 'a) \<Rightarrow> 'a ref \<Rightarrow> 'a list \<Rightarrow> 'a ref \<Rightarrow> bool" |
49 primrec |
65 primrec |
50 "path h x [] y = (x = y)" |
66 "path h x [] y = (x = y)" |
51 "path h x (a#as) y = (x = Some a \<and> path h (h a) as y)" |
67 "path h x (a#as) y = (x = Ref a \<and> path h (h a) as y)" |
52 |
68 |
53 lemma [iff]: "path h None xs y = (xs = [] \<and> y = None)" |
69 lemma [iff]: "path h Null xs y = (xs = [] \<and> y = Null)" |
54 apply(case_tac xs) |
70 apply(case_tac xs) |
55 apply fastsimp |
71 apply fastsimp |
56 apply fastsimp |
72 apply fastsimp |
57 done |
73 done |
58 |
74 |
59 lemma [simp]: "path h (Some a) as z = |
75 lemma [simp]: "path h (Ref a) as z = |
60 (as = [] \<and> z = Some a \<or> (\<exists>bs. as = a#bs \<and> path h (h a) bs z))" |
76 (as = [] \<and> z = Ref a \<or> (\<exists>bs. as = a#bs \<and> path h (h a) bs z))" |
61 apply(case_tac as) |
77 apply(case_tac as) |
62 apply fastsimp |
78 apply fastsimp |
63 apply fastsimp |
79 apply fastsimp |
64 done |
80 done |
65 |
81 |
71 |
87 |
72 subsection "Lists on the heap" |
88 subsection "Lists on the heap" |
73 |
89 |
74 constdefs |
90 constdefs |
75 list :: "('a \<leadsto> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> bool" |
91 list :: "('a \<leadsto> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> bool" |
76 "list h x as == path h x as None" |
92 "list h x as == path h x as Null" |
77 |
93 |
78 lemma [simp]: "list h x [] = (x = None)" |
94 lemma [simp]: "list h x [] = (x = Null)" |
79 by(simp add:list_def) |
95 by(simp add:list_def) |
80 |
96 |
81 lemma [simp]: "list h x (a#as) = (x = Some a \<and> list h (h a) as)" |
97 lemma [simp]: "list h x (a#as) = (x = Ref a \<and> list h (h a) as)" |
82 by(simp add:list_def) |
98 by(simp add:list_def) |
83 |
99 |
84 lemma [simp]: "list h None as = (as = [])" |
100 lemma [simp]: "list h Null as = (as = [])" |
85 by(case_tac as, simp_all) |
101 by(case_tac as, simp_all) |
86 |
102 |
87 lemma [simp]: "list h (Some a) as = (\<exists>bs. as = a#bs \<and> list h (h a) bs)" |
103 lemma [simp]: "list h (Ref a) as = (\<exists>bs. as = a#bs \<and> list h (h a) bs)" |
88 by(case_tac as, simp_all, fast) |
104 by(case_tac as, simp_all, fast) |
89 |
105 |
90 |
106 |
91 declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp] |
107 declare fun_upd_apply[simp del]fun_upd_same[simp] fun_upd_other[simp] |
92 |
108 |
115 done |
131 done |
116 |
132 |
117 lemma [simp]: "list h (h a) as \<Longrightarrow> list (h(a := y)) (h a) as" |
133 lemma [simp]: "list h (h a) as \<Longrightarrow> list (h(a := y)) (h a) as" |
118 by(simp add:list_hd_not_in_tl) |
134 by(simp add:list_hd_not_in_tl) |
119 (* Note that the opposite direction does NOT hold: |
135 (* Note that the opposite direction does NOT hold: |
120 If h = (a \<mapsto> Some a) |
136 If h = (a \<mapsto> Ref a) |
121 then list (h(a := None)) (h a) [a] |
137 then list (h(a := Null)) (h a) [a] |
122 but not list h (h a) [] (because h is cyclic) |
138 but not list h (h a) [] (because h is cyclic) |
123 *) |
139 *) |
124 |
140 |
125 section"Hoare logic" |
141 section "Verifications" |
126 |
142 |
127 subsection"List reversal" |
143 subsection "List reversal" |
128 |
144 |
129 text{* A tactic script: *} |
145 text "A short but unreadable proof:" |
130 |
146 |
131 lemma "|- VARS tl p q r. |
147 lemma "|- VARS tl p q r. |
132 {list tl p As \<and> list tl q Bs \<and> set As \<inter> set Bs = {}} |
148 {list tl p Ps \<and> list tl q Qs \<and> set Ps \<inter> set Qs = {}} |
133 WHILE p \<noteq> None |
149 WHILE p \<noteq> Null |
134 INV {\<exists>As' Bs'. list tl p As' \<and> list tl q Bs' \<and> set As' \<inter> set Bs' = {} \<and> |
150 INV {\<exists>ps qs. list tl p ps \<and> list tl q qs \<and> set ps \<inter> set qs = {} \<and> |
135 rev As' @ Bs' = rev As @ Bs} |
151 rev ps @ qs = rev Ps @ Qs} |
136 DO r := p; p := p^:tl; r^.tl := q; q := r OD |
152 DO r := p; p := p^.tl; r^.tl := q; q := r OD |
137 {list tl q (rev As @ Bs)}" |
153 {list tl q (rev Ps @ Qs)}" |
138 apply vcg_simp |
154 apply vcg_simp |
139 |
155 apply fastsimp |
140 apply(rule_tac x = As in exI) |
156 apply clarify |
141 apply simp |
157 apply(rename_tac ps b qs) |
142 |
158 apply clarsimp |
143 apply clarify |
159 apply(rename_tac ps') |
144 apply(rename_tac As' b Bs') |
160 apply(rule_tac x = ps' in exI) |
145 apply clarsimp |
161 apply simp |
146 apply(rename_tac As'') |
162 apply(rule_tac x = "b#qs" in exI) |
147 apply(rule_tac x = As'' in exI) |
163 apply simp |
148 apply simp |
164 apply fastsimp |
149 apply(rule_tac x = "b#Bs'" in exI) |
165 done |
150 apply simp |
166 |
151 |
167 |
152 apply clarsimp |
168 text "A longer readable version:" |
153 done |
|
154 |
|
155 text{*A readable(?) proof: *} |
|
156 |
169 |
157 lemma "|- VARS tl p q r. |
170 lemma "|- VARS tl p q r. |
158 {list tl p As \<and> list tl q Bs \<and> set As \<inter> set Bs = {}} |
171 {list tl p Ps \<and> list tl q Qs \<and> set Ps \<inter> set Qs = {}} |
159 WHILE p \<noteq> None |
172 WHILE p \<noteq> Null |
160 INV {\<exists>As' Bs'. list tl p As' \<and> list tl q Bs' \<and> set As' \<inter> set Bs' = {} \<and> |
173 INV {\<exists>ps qs. list tl p ps \<and> list tl q qs \<and> set ps \<inter> set qs = {} \<and> |
161 rev As' @ Bs' = rev As @ Bs} |
174 rev ps @ qs = rev Ps @ Qs} |
162 DO r := p; p := p^:tl; r^.tl := q; q := r OD |
175 DO r := p; p := p^.tl; r^.tl := q; q := r OD |
163 {list tl q (rev As @ Bs)}" |
176 {list tl q (rev Ps @ Qs)}" |
164 (is "Valid {(tl,p,q,r).?P tl p q r} |
|
165 (While _ {(tl,p,q,r). \<exists>As' Bs'. ?I tl p q r As' Bs'} _) |
|
166 {(tl,p,q,r).?Q tl p q r}") |
|
167 proof vcg |
177 proof vcg |
168 fix tl p q r |
178 fix tl p q r |
169 assume "?P tl p q r" |
179 assume "list tl p Ps \<and> list tl q Qs \<and> set Ps \<inter> set Qs = {}" |
170 hence "?I tl p q r As Bs" by simp |
180 thus "\<exists>ps qs. list tl p ps \<and> list tl q qs \<and> set ps \<inter> set qs = {} \<and> |
171 thus "\<exists>As' Bs'. ?I tl p q r As' Bs'" by rules |
181 rev ps @ qs = rev Ps @ Qs" by fastsimp |
172 next |
182 next |
173 fix tl p q r |
183 fix tl p q r |
174 assume "(\<exists>As' Bs'. ?I tl p q r As' Bs') \<and> p \<noteq> None" |
184 assume "(\<exists>ps qs. list tl p ps \<and> list tl q qs \<and> set ps \<inter> set qs = {} \<and> |
175 then obtain As' Bs' a where I: "?I tl p q r As' Bs'" "p = Some a" by fast |
185 rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null" |
176 then obtain As'' where "As' = a # As''" by fastsimp |
186 (is "(\<exists>ps qs. ?I ps qs) \<and> _") |
177 hence "?I (tl(the p := q)) (p^:tl) p p As'' (a#Bs')" using I by fastsimp |
187 then obtain ps qs a where I: "?I ps qs \<and> p = Ref a" |
178 thus "\<exists>As' Bs'. ?I (tl(the p := q)) (p^:tl) p p As' Bs'" by rules |
188 by fast |
|
189 then obtain ps' where "ps = a # ps'" by fastsimp |
|
190 hence "list (tl(p \<rightarrow> q)) (p^.tl) ps' \<and> |
|
191 list (tl(p \<rightarrow> q)) p (a#qs) \<and> |
|
192 set ps' \<inter> set (a#qs) = {} \<and> |
|
193 rev ps' @ (a#qs) = rev Ps @ Qs" |
|
194 using I by fastsimp |
|
195 thus "\<exists>ps' qs'. list (tl(p \<rightarrow> q)) (p^.tl) ps' \<and> |
|
196 list (tl(p \<rightarrow> q)) p qs' \<and> |
|
197 set ps' \<inter> set qs' = {} \<and> |
|
198 rev ps' @ qs' = rev Ps @ Qs" by fast |
179 next |
199 next |
180 fix tl p q r |
200 fix tl p q r |
181 assume "(\<exists>As' Bs'. ?I tl p q r As' Bs') \<and> \<not> p \<noteq> None" |
201 assume "(\<exists>ps qs. list tl p ps \<and> list tl q qs \<and> set ps \<inter> set qs = {} \<and> |
182 thus "?Q tl p q r" by clarsimp |
202 rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null" |
|
203 thus "list tl q (rev Ps @ Qs)" by fastsimp |
183 qed |
204 qed |
184 |
205 |
185 |
206 |
186 subsection{*Searching in a list*} |
207 subsection "Searching in a list" |
187 |
208 |
188 text{*What follows is a sequence of successively more intelligent proofs that |
209 text{*What follows is a sequence of successively more intelligent proofs that |
189 a simple loop finds an element in a linked list. |
210 a simple loop finds an element in a linked list. |
190 |
211 |
191 We start with a proof based on the @{term list} predicate. This means it only |
212 We start with a proof based on the @{term list} predicate. This means it only |
192 works for acyclic lists. *} |
213 works for acyclic lists. *} |
193 |
214 |
194 lemma "|- VARS tl p. |
215 lemma "|- VARS tl p. |
195 {list tl p As \<and> X \<in> set As} |
216 {list tl p Ps \<and> X \<in> set Ps} |
196 WHILE p \<noteq> None \<and> p \<noteq> Some X |
217 WHILE p \<noteq> Null \<and> p \<noteq> Ref X |
197 INV {p \<noteq> None \<and> (\<exists>As'. list tl p As' \<and> X \<in> set As')} |
218 INV {p \<noteq> Null \<and> (\<exists>ps. list tl p ps \<and> X \<in> set ps)} |
198 DO p := p^:tl OD |
219 DO p := p^.tl OD |
199 {p = Some X}" |
220 {p = Ref X}" |
200 apply vcg_simp |
221 apply vcg_simp |
201 apply(case_tac p) |
222 apply(case_tac p) |
202 apply clarsimp |
223 apply clarsimp |
203 apply fastsimp |
224 apply fastsimp |
204 apply clarsimp |
225 apply clarsimp |
260 done |
281 done |
261 |
282 |
262 text{*Finally, the simplest version, based on a relation on type @{typ 'a}:*} |
283 text{*Finally, the simplest version, based on a relation on type @{typ 'a}:*} |
263 |
284 |
264 lemma "|- VARS tl p. |
285 lemma "|- VARS tl p. |
265 {p \<noteq> None \<and> X \<in> ({(x,y). tl x = Some y}^* `` {the p})} |
286 {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {the p})} |
266 WHILE p \<noteq> None \<and> p \<noteq> Some X |
287 WHILE p \<noteq> Null \<and> p \<noteq> Ref X |
267 INV {p \<noteq> None \<and> X \<in> ({(x,y). tl x = Some y}^* `` {the p})} |
288 INV {p \<noteq> Null \<and> X \<in> ({(x,y). tl x = Ref y}^* `` {the p})} |
268 DO p := p^:tl OD |
289 DO p := p^.tl OD |
269 {p = Some X}" |
290 {p = Ref X}" |
270 apply vcg_simp |
291 apply vcg_simp |
271 apply clarsimp |
292 apply clarsimp |
272 apply(erule converse_rtranclE) |
293 apply(erule converse_rtranclE) |
273 apply simp |
294 apply simp |
274 apply clarsimp |
295 apply clarsimp |
275 apply clarsimp |
296 apply clarsimp |
276 done |
297 done |
277 |
298 |
278 subsection{*Merging two lists*} |
299 subsection "Merging two lists" |
279 |
300 |
280 consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" |
301 consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" |
281 |
302 |
282 recdef merge "measure(%(xs,ys,f). size xs + size ys)" |
303 recdef merge "measure(%(xs,ys,f). size xs + size ys)" |
283 "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f) |
304 "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f) |
291 |
312 |
292 declare imp_disjL[simp del] imp_disjCL[simp] |
313 declare imp_disjL[simp del] imp_disjCL[simp] |
293 |
314 |
294 lemma "|- VARS hd tl p q r s. |
315 lemma "|- VARS hd tl p q r s. |
295 {list tl p Ps \<and> list tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> |
316 {list tl p Ps \<and> list tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> |
296 (p \<noteq> None \<or> q \<noteq> None)} |
317 (p \<noteq> Null \<or> q \<noteq> Null)} |
297 IF if q = None then True else p \<noteq> None \<and> p^:hd \<le> q^:hd |
318 IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd |
298 THEN r := p; p := p^:tl ELSE r := q; q := q^:tl FI; |
319 THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI; |
299 s := r; |
320 s := r; |
300 WHILE p \<noteq> None \<or> q \<noteq> None |
321 WHILE p \<noteq> Null \<or> q \<noteq> Null |
301 INV {EX rs ps qs a. path tl r rs s \<and> list tl p ps \<and> list tl q qs \<and> |
322 INV {EX rs ps qs a. path tl r rs s \<and> list tl p ps \<and> list tl q qs \<and> |
302 distinct(a # ps @ qs @ rs) \<and> s = Some a \<and> |
323 distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and> |
303 merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) = |
324 merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) = |
304 rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and> |
325 rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and> |
305 (tl a = p \<or> tl a = q)} |
326 (tl a = p \<or> tl a = q)} |
306 DO IF if q = None then True else p \<noteq> None \<and> p^:hd \<le> q^:hd |
327 DO IF if q = Null then True else p \<noteq> Null \<and> p^.hd \<le> q^.hd |
307 THEN s^.tl := p; p := p^:tl ELSE s^.tl := q; q := q^:tl FI; |
328 THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI; |
308 s := s^:tl |
329 s := s^.tl |
309 OD |
330 OD |
310 {list tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}" |
331 {list tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}" |
311 apply vcg_simp |
332 apply vcg_simp |
312 |
333 |
313 apply (fastsimp) |
334 apply (fastsimp) |