author | oheimb |
Thu, 09 Aug 2001 20:48:57 +0200 | |
changeset 11497 | 0e66e0114d9a |
parent 11376 | bf98ad1c22c6 |
child 11499 | 7a7bb59a05db |
permissions | -rw-r--r-- |
11376 | 1 |
(* Title: HOL/NanoJava/State.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 2001 Technische Universitaet Muenchen |
|
5 |
*) |
|
6 |
||
7 |
header "Program State" |
|
8 |
||
9 |
theory State = TypeRel: |
|
10 |
||
11 |
constdefs |
|
12 |
||
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11376
diff
changeset
|
13 |
body :: "imname => stmt" |
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11376
diff
changeset
|
14 |
"body \<equiv> \<lambda>(C,m). bdy (the (method C m))" |
11376 | 15 |
|
16 |
text {* locations, i.e.\ abstract references to objects *} |
|
17 |
typedecl loc |
|
18 |
arities loc :: "term" |
|
19 |
||
20 |
datatype val |
|
21 |
= Null (* null reference *) |
|
22 |
| Addr loc (* address, i.e. location of object *) |
|
23 |
||
24 |
types fields |
|
25 |
= "(vnam \<leadsto> val)" |
|
26 |
||
27 |
obj = "cname \<times> fields" |
|
28 |
||
29 |
translations |
|
30 |
||
31 |
"fields" \<leftharpoondown> (type)"vnam \<Rightarrow> val option" |
|
32 |
"obj" \<leftharpoondown> (type)"cname \<times> fields" |
|
33 |
||
34 |
constdefs |
|
35 |
||
36 |
init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)" |
|
37 |
"init_vars m == option_map (\<lambda>T. Null) o m" |
|
38 |
||
39 |
text {* private *} |
|
40 |
types heap = "loc \<leadsto> obj" |
|
41 |
locals = "vname \<leadsto> val" |
|
42 |
||
43 |
text {* private *} |
|
44 |
record state |
|
45 |
= heap :: heap |
|
46 |
locals :: locals |
|
47 |
||
48 |
translations |
|
49 |
||
50 |
"heap" \<leftharpoondown> (type)"loc => obj option" |
|
51 |
"locals" \<leftharpoondown> (type)"vname => val option" |
|
52 |
"state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)" |
|
53 |
||
54 |
constdefs |
|
55 |
||
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11376
diff
changeset
|
56 |
reset_locs :: "state => state" |
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11376
diff
changeset
|
57 |
"reset_locs s \<equiv> s (| locals := empty |)" |
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11376
diff
changeset
|
58 |
|
11376 | 59 |
init_locs :: "cname => mname => state => state" |
11497
0e66e0114d9a
corrected initialization of locals, streamlined Impl
oheimb
parents:
11376
diff
changeset
|
60 |
"init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m)))) |)" |
11376 | 61 |
|
62 |
text {* The first parameter of @{term set_locs} is of type @{typ state} |
|
63 |
rather than @{typ locals} in order to keep @{typ locals} private.*} |
|
64 |
constdefs |
|
65 |
set_locs :: "state => state => state" |
|
66 |
"set_locs s s' \<equiv> s' (| locals := locals s |)" |
|
67 |
||
68 |
get_local :: "state => vname => val" ("_<_>" [99,0] 99) |
|
69 |
"get_local s x \<equiv> the (locals s x)" |
|
70 |
||
71 |
(* local function: *) |
|
72 |
get_obj :: "state => loc => obj" |
|
73 |
"get_obj s a \<equiv> the (heap s a)" |
|
74 |
||
75 |
obj_class :: "state => loc => cname" |
|
76 |
"obj_class s a \<equiv> fst (get_obj s a)" |
|
77 |
||
78 |
get_field :: "state => loc => vnam => val" |
|
79 |
"get_field s a f \<equiv> the (snd (get_obj s a) f)" |
|
80 |
||
81 |
constdefs |
|
82 |
||
83 |
(* local function: *) |
|
84 |
hupd :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state" ("hupd'(_|->_')" [10,10] 1000) |
|
85 |
"hupd a obj s \<equiv> s (| heap := ((heap s)(a\<mapsto>obj))|)" |
|
86 |
||
87 |
lupd :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_|->_')" [10,10] 1000) |
|
88 |
"lupd x v s \<equiv> s (| locals := ((locals s)(x\<mapsto>v ))|)" |
|
89 |
||
90 |
syntax (xsymbols) |
|
91 |
hupd :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state" ("hupd'(_\<mapsto>_')" [10,10] 1000) |
|
92 |
lupd :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_\<mapsto>_')" [10,10] 1000) |
|
93 |
||
94 |
constdefs |
|
95 |
||
96 |
new_obj :: "loc \<Rightarrow> cname \<Rightarrow> state \<Rightarrow> state" |
|
97 |
"new_obj a C \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))" |
|
98 |
||
99 |
upd_obj :: "loc \<Rightarrow> vnam \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" |
|
100 |
"upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s" |
|
101 |
||
102 |
new_Addr :: "state => val" |
|
103 |
"new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null" |
|
104 |
||
105 |
lemma new_AddrD: |
|
106 |
"new_Addr s = v \<Longrightarrow> (\<exists>a. v = Addr a \<and> heap s a = None) | v = Null" |
|
107 |
apply (unfold new_Addr_def) |
|
108 |
apply (erule subst) |
|
109 |
apply (rule someI) |
|
110 |
apply (rule disjI2) |
|
111 |
apply (rule HOL.refl) |
|
112 |
done |
|
113 |
||
114 |
end |