|
1 (* Title: HOL/Hoare/HeapSyntax.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2002 TUM |
|
5 *) |
|
6 |
|
7 theory HeapSyntaxAbort = HoareAbort + Heap: |
|
8 |
|
9 subsection "Field access and update" |
|
10 |
|
11 text{* Heap update @{text"p^.h := e"} is now guarded against @{term p} |
|
12 being Null. However, @{term p} may still be illegal, |
|
13 e.g. uninitialized or dangling. To guard against that, one needs a |
|
14 more detailed model of the heap where allocated and free addresses are |
|
15 distinguished, e.g. by making the heap a map, or by carrying the set |
|
16 of free addresses around. This is needed anyway as soon as we want to |
|
17 reason about storage allocation/deallocation. *} |
|
18 |
|
19 syntax |
|
20 "refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" |
|
21 ("_/'((_ \<rightarrow> _)')" [1000,0] 900) |
|
22 "@fassign" :: "'a ref => id => 'v => 's com" |
|
23 ("(2_^._ :=/ _)" [70,1000,65] 61) |
|
24 "@faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v" |
|
25 ("_^._" [65,1000] 65) |
|
26 translations |
|
27 "refupdate f r v" == "f(addr r := v)" |
|
28 "p^.f := e" => "(p \<noteq> Null) \<rightarrow> (f := refupdate f p e)" |
|
29 "p^.f" => "f(addr p)" |
|
30 |
|
31 |
|
32 declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp] |
|
33 |
|
34 |
|
35 text "An example due to Suzuki:" |
|
36 |
|
37 lemma "VARS v n |
|
38 {w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 & |
|
39 distinct[w0,x0,y0,z0]} |
|
40 w^.v := (1::int); w^.n := x; |
|
41 x^.v := 2; x^.n := y; |
|
42 y^.v := 3; y^.n := z; |
|
43 z^.v := 4; x^.n := z |
|
44 {w^.n^.n^.v = 4}" |
|
45 by vcg_simp |
|
46 |
|
47 end |