15 |
15 |
16 text {* locations, i.e.\ abstract references to objects *} |
16 text {* locations, i.e.\ abstract references to objects *} |
17 typedecl loc |
17 typedecl loc |
18 |
18 |
19 datatype val |
19 datatype val |
20 = Null (* null reference *) |
20 = Null --{* null reference *} |
21 | Addr loc (* address, i.e. location of object *) |
21 | Addr loc --{* address, i.e. location of object *} |
22 |
22 |
23 types fields |
23 types fields |
24 = "(vnam \<leadsto> val)" |
24 = "(fname \<leadsto> val)" |
25 |
25 |
26 obj = "cname \<times> fields" |
26 obj = "cname \<times> fields" |
27 |
27 |
28 translations |
28 translations |
29 |
29 |
30 "fields" \<leftharpoondown> (type)"vnam \<Rightarrow> val option" |
30 "fields" \<leftharpoondown> (type)"fname => val option" |
31 "obj" \<leftharpoondown> (type)"cname \<times> fields" |
31 "obj" \<leftharpoondown> (type)"cname \<times> fields" |
32 |
32 |
33 constdefs |
33 constdefs |
34 |
34 |
35 init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)" |
35 init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)" |
65 "set_locs s s' \<equiv> s' (| locals := locals s |)" |
65 "set_locs s s' \<equiv> s' (| locals := locals s |)" |
66 |
66 |
67 get_local :: "state => vname => val" ("_<_>" [99,0] 99) |
67 get_local :: "state => vname => val" ("_<_>" [99,0] 99) |
68 "get_local s x \<equiv> the (locals s x)" |
68 "get_local s x \<equiv> the (locals s x)" |
69 |
69 |
70 (* local function: *) |
70 --{* local function: *} |
71 get_obj :: "state => loc => obj" |
71 get_obj :: "state => loc => obj" |
72 "get_obj s a \<equiv> the (heap s a)" |
72 "get_obj s a \<equiv> the (heap s a)" |
73 |
73 |
74 obj_class :: "state => loc => cname" |
74 obj_class :: "state => loc => cname" |
75 "obj_class s a \<equiv> fst (get_obj s a)" |
75 "obj_class s a \<equiv> fst (get_obj s a)" |
76 |
76 |
77 get_field :: "state => loc => vnam => val" |
77 get_field :: "state => loc => fname => val" |
78 "get_field s a f \<equiv> the (snd (get_obj s a) f)" |
78 "get_field s a f \<equiv> the (snd (get_obj s a) f)" |
|
79 |
|
80 --{* local function: *} |
|
81 hupd :: "loc => obj => state => state" ("hupd'(_|->_')" [10,10] 1000) |
|
82 "hupd a obj s \<equiv> s (| heap := ((heap s)(a\<mapsto>obj))|)" |
|
83 |
|
84 lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000) |
|
85 "lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)" |
|
86 |
|
87 syntax (xsymbols) |
|
88 hupd :: "loc => obj => state => state" ("hupd'(_\<mapsto>_')" [10,10] 1000) |
|
89 lupd :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000) |
79 |
90 |
80 constdefs |
91 constdefs |
81 |
92 |
82 (* local function: *) |
93 new_obj :: "loc => cname => state => state" |
83 hupd :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state" ("hupd'(_|->_')" [10,10] 1000) |
|
84 "hupd a obj s \<equiv> s (| heap := ((heap s)(a\<mapsto>obj))|)" |
|
85 |
|
86 lupd :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_|->_')" [10,10] 1000) |
|
87 "lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)" |
|
88 |
|
89 syntax (xsymbols) |
|
90 hupd :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state" ("hupd'(_\<mapsto>_')" [10,10] 1000) |
|
91 lupd :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_\<mapsto>_')" [10,10] 1000) |
|
92 |
|
93 constdefs |
|
94 |
|
95 new_obj :: "loc \<Rightarrow> cname \<Rightarrow> state \<Rightarrow> state" |
|
96 "new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))" |
94 "new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))" |
97 |
95 |
98 upd_obj :: "loc \<Rightarrow> vnam \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" |
96 upd_obj :: "loc => fname => val => state => state" |
99 "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s" |
97 "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s" |
100 |
98 |
101 new_Addr :: "state => val" |
99 new_Addr :: "state => val" |
102 "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null" |
100 "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null" |
103 |
101 |