author | wenzelm |
Wed, 22 Apr 2020 19:22:43 +0200 | |
changeset 71787 | acfe72ff00c2 |
parent 69597 | ff784d5a5bfb |
child 72990 | db8f94656024 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Hoare/HeapSyntaxAbort.thy |
13875 | 2 |
Author: Tobias Nipkow |
3 |
Copyright 2002 TUM |
|
4 |
*) |
|
5 |
||
35316
870dfea4f9c0
dropped axclass; dropped Id; session theory Hoare.thy
haftmann
parents:
35113
diff
changeset
|
6 |
theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin |
13875 | 7 |
|
8 |
subsection "Field access and update" |
|
9 |
||
69597 | 10 |
text\<open>Heap update \<open>p^.h := e\<close> is now guarded against \<^term>\<open>p\<close> |
11 |
being Null. However, \<^term>\<open>p\<close> may still be illegal, |
|
13875 | 12 |
e.g. uninitialized or dangling. To guard against that, one needs a |
13 |
more detailed model of the heap where allocated and free addresses are |
|
14 |
distinguished, e.g. by making the heap a map, or by carrying the set |
|
15 |
of free addresses around. This is needed anyway as soon as we want to |
|
62042 | 16 |
reason about storage allocation/deallocation.\<close> |
13875 | 17 |
|
18 |
syntax |
|
35101 | 19 |
"_refupdate" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a ref \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" |
13875 | 20 |
("_/'((_ \<rightarrow> _)')" [1000,0] 900) |
35101 | 21 |
"_fassign" :: "'a ref => id => 'v => 's com" |
13875 | 22 |
("(2_^._ :=/ _)" [70,1000,65] 61) |
35101 | 23 |
"_faccess" :: "'a ref => ('a ref \<Rightarrow> 'v) => 'v" |
13875 | 24 |
("_^._" [65,1000] 65) |
25 |
translations |
|
35113 | 26 |
"_refupdate f r v" == "f(CONST addr r := v)" |
27 |
"p^.f := e" => "(p \<noteq> CONST Null) \<rightarrow> (f := _refupdate f p e)" |
|
28 |
"p^.f" => "f(CONST addr p)" |
|
13875 | 29 |
|
30 |
||
31 |
declare fun_upd_apply[simp del] fun_upd_same[simp] fun_upd_other[simp] |
|
32 |
||
33 |
||
34 |
text "An example due to Suzuki:" |
|
35 |
||
36 |
lemma "VARS v n |
|
37 |
{w = Ref w0 & x = Ref x0 & y = Ref y0 & z = Ref z0 & |
|
38 |
distinct[w0,x0,y0,z0]} |
|
39 |
w^.v := (1::int); w^.n := x; |
|
40 |
x^.v := 2; x^.n := y; |
|
41 |
y^.v := 3; y^.n := z; |
|
42 |
z^.v := 4; x^.n := z |
|
43 |
{w^.n^.n^.v = 4}" |
|
44 |
by vcg_simp |
|
45 |
||
46 |
end |