68 |
68 |
69 definition get_field :: "state => loc => fname => val" where |
69 definition get_field :: "state => loc => fname => val" where |
70 "get_field s a f \<equiv> the (snd (get_obj s a) f)" |
70 "get_field s a f \<equiv> the (snd (get_obj s a) f)" |
71 |
71 |
72 --{* local function: *} |
72 --{* local function: *} |
73 definition hupd :: "loc => obj => state => state" ("hupd'(_|->_')" [10,10] 1000) where |
73 definition hupd :: "loc => obj => state => state" ("hupd'(_\<mapsto>_')" [10,10] 1000) where |
74 "hupd a obj s \<equiv> s (| heap := ((heap s)(a\<mapsto>obj))|)" |
74 "hupd a obj s \<equiv> s (| heap := ((heap s)(a\<mapsto>obj))|)" |
75 |
75 |
76 definition lupd :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000) where |
76 definition lupd :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000) where |
77 "lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)" |
77 "lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)" |
78 |
|
79 notation (xsymbols) |
|
80 hupd ("hupd'(_\<mapsto>_')" [10,10] 1000) and |
|
81 lupd ("lupd'(_\<mapsto>_')" [10,10] 1000) |
|
82 |
78 |
83 definition new_obj :: "loc => cname => state => state" where |
79 definition new_obj :: "loc => cname => state => state" where |
84 "new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))" |
80 "new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))" |
85 |
81 |
86 definition upd_obj :: "loc => fname => val => state => state" where |
82 definition upd_obj :: "loc => fname => val => state => state" where |