author | oheimb |
Wed, 03 Apr 2002 10:21:13 +0200 | |
changeset 13076 | 70704dd48bd5 |
parent 12925 | 99131847fb93 |
child 13688 | a0b16d42d489 |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/Conform.thy |
12854 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb |
|
12858 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
12854 | 5 |
*) |
6 |
||
7 |
header {* Conformance notions for the type soundness proof for Java *} |
|
8 |
||
9 |
theory Conform = State: |
|
10 |
||
11 |
text {* |
|
12 |
design issues: |
|
13 |
\begin{itemize} |
|
14 |
\item lconf allows for (arbitrary) inaccessible values |
|
15 |
\item ''conforms'' does not directly imply that the dynamic types of all |
|
16 |
objects on the heap are indeed existing classes. Yet this can be |
|
17 |
inferred for all referenced objs. |
|
18 |
\end{itemize} |
|
19 |
*} |
|
20 |
||
21 |
types env_ = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *) |
|
22 |
||
23 |
||
24 |
section "extension of global store" |
|
25 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
26 |
|
12854 | 27 |
constdefs |
28 |
||
29 |
gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_" [71,71] 70) |
|
30 |
"s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj" |
|
31 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
32 |
text {* For the the proof of type soundness we will need the |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
33 |
property that during execution, objects are not lost and moreover retain the |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
34 |
values of their tags. So the object store grows conservatively. Note that if |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
35 |
we considered garbage collection, we would have to restrict this property to |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
36 |
accessible objects. |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
37 |
*} |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
38 |
|
12854 | 39 |
lemma gext_objD: |
40 |
"\<lbrakk>s\<le>|s'; globs s r = Some obj\<rbrakk> |
|
41 |
\<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj" |
|
42 |
apply (simp only: gext_def) |
|
43 |
by force |
|
44 |
||
45 |
lemma rev_gext_objD: |
|
46 |
"\<lbrakk>globs s r = Some obj; s\<le>|s'\<rbrakk> |
|
47 |
\<Longrightarrow> \<exists>obj'. globs s' r = Some obj' \<and> tag obj' = tag obj" |
|
48 |
by (auto elim: gext_objD) |
|
49 |
||
50 |
lemma init_class_obj_inited: |
|
51 |
"init_class_obj G C s1\<le>|s2 \<Longrightarrow> inited C (globs s2)" |
|
52 |
apply (unfold inited_def init_obj_def) |
|
53 |
apply (auto dest!: gext_objD) |
|
54 |
done |
|
55 |
||
56 |
lemma gext_refl [intro!, simp]: "s\<le>|s" |
|
57 |
apply (unfold gext_def) |
|
58 |
apply (fast del: fst_splitE) |
|
59 |
done |
|
60 |
||
61 |
lemma gext_gupd [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|gupd(r\<mapsto>x)s" |
|
62 |
by (auto simp: gext_def) |
|
63 |
||
64 |
lemma gext_new [simp, elim!]: "\<And>s. globs s r = None \<Longrightarrow> s\<le>|init_obj G oi r s" |
|
65 |
apply (simp only: init_obj_def) |
|
66 |
apply (erule_tac gext_gupd) |
|
67 |
done |
|
68 |
||
69 |
lemma gext_trans [elim]: "\<And>X. \<lbrakk>s\<le>|s'; s'\<le>|s''\<rbrakk> \<Longrightarrow> s\<le>|s''" |
|
70 |
by (force simp: gext_def) |
|
71 |
||
72 |
lemma gext_upd_gobj [intro!]: "s\<le>|upd_gobj r n v s" |
|
73 |
apply (simp only: gext_def) |
|
74 |
apply auto |
|
75 |
apply (case_tac "ra = r") |
|
76 |
apply auto |
|
77 |
apply (case_tac "globs s r = None") |
|
78 |
apply auto |
|
79 |
done |
|
80 |
||
81 |
lemma gext_cong1 [simp]: "set_locals l s1\<le>|s2 = s1\<le>|s2" |
|
82 |
by (auto simp: gext_def) |
|
83 |
||
84 |
lemma gext_cong2 [simp]: "s1\<le>|set_locals l s2 = s1\<le>|s2" |
|
85 |
by (auto simp: gext_def) |
|
86 |
||
87 |
||
88 |
lemma gext_lupd1 [simp]: "lupd(vn\<mapsto>v)s1\<le>|s2 = s1\<le>|s2" |
|
89 |
by (auto simp: gext_def) |
|
90 |
||
91 |
lemma gext_lupd2 [simp]: "s1\<le>|lupd(vn\<mapsto>v)s2 = s1\<le>|s2" |
|
92 |
by (auto simp: gext_def) |
|
93 |
||
94 |
||
95 |
lemma inited_gext: "\<lbrakk>inited C (globs s); s\<le>|s'\<rbrakk> \<Longrightarrow> inited C (globs s')" |
|
96 |
apply (unfold inited_def) |
|
97 |
apply (auto dest: gext_objD) |
|
98 |
done |
|
99 |
||
100 |
||
101 |
section "value conformance" |
|
102 |
||
103 |
constdefs |
|
104 |
||
105 |
conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_" [71,71,71,71] 70) |
|
106 |
"G,s\<turnstile>v\<Colon>\<preceq>T \<equiv> \<exists>T'\<in>typeof (\<lambda>a. option_map obj_ty (heap s a)) v:G\<turnstile>T'\<preceq>T" |
|
107 |
||
108 |
lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T" |
|
109 |
by (auto simp: conf_def) |
|
110 |
||
111 |
lemma conf_lupd [simp]: "G,lupd(vn\<mapsto>va)s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T" |
|
112 |
by (auto simp: conf_def) |
|
113 |
||
114 |
lemma conf_PrimT [simp]: "\<forall>dt. typeof dt v = Some (PrimT t) \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>PrimT t" |
|
115 |
apply (simp add: conf_def) |
|
116 |
done |
|
117 |
||
118 |
lemma conf_litval [rule_format (no_asm)]: |
|
119 |
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T" |
|
120 |
apply (unfold conf_def) |
|
121 |
apply (rule val.induct) |
|
122 |
apply auto |
|
123 |
done |
|
124 |
||
125 |
lemma conf_Null [simp]: "G,s\<turnstile>Null\<Colon>\<preceq>T = G\<turnstile>NT\<preceq>T" |
|
126 |
by (simp add: conf_def) |
|
127 |
||
128 |
lemma conf_Addr: |
|
129 |
"G,s\<turnstile>Addr a\<Colon>\<preceq>T = (\<exists>obj. heap s a = Some obj \<and> G\<turnstile>obj_ty obj\<preceq>T)" |
|
130 |
by (auto simp: conf_def) |
|
131 |
||
132 |
lemma conf_AddrI:"\<lbrakk>heap s a = Some obj; G\<turnstile>obj_ty obj\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>T" |
|
133 |
apply (rule conf_Addr [THEN iffD2]) |
|
134 |
by fast |
|
135 |
||
136 |
lemma defval_conf [rule_format (no_asm), elim]: |
|
137 |
"is_type G T \<longrightarrow> G,s\<turnstile>default_val T\<Colon>\<preceq>T" |
|
138 |
apply (unfold conf_def) |
|
139 |
apply (induct "T") |
|
140 |
apply (auto intro: prim_ty.induct) |
|
141 |
done |
|
142 |
||
143 |
lemma conf_widen [rule_format (no_asm), elim]: |
|
144 |
"G\<turnstile>T\<preceq>T' \<Longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T \<longrightarrow> ws_prog G \<longrightarrow> G,s\<turnstile>x\<Colon>\<preceq>T'" |
|
145 |
apply (unfold conf_def) |
|
146 |
apply (rule val.induct) |
|
147 |
apply (auto elim: ws_widen_trans) |
|
148 |
done |
|
149 |
||
150 |
lemma conf_gext [rule_format (no_asm), elim]: |
|
151 |
"G,s\<turnstile>v\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> G,s'\<turnstile>v\<Colon>\<preceq>T" |
|
152 |
apply (unfold gext_def conf_def) |
|
153 |
apply (rule val.induct) |
|
154 |
apply force+ |
|
155 |
done |
|
156 |
||
157 |
||
158 |
lemma conf_list_widen [rule_format (no_asm)]: |
|
159 |
"ws_prog G \<Longrightarrow> |
|
160 |
\<forall>Ts Ts'. list_all2 (conf G s) vs Ts |
|
161 |
\<longrightarrow> G\<turnstile>Ts[\<preceq>] Ts' \<longrightarrow> list_all2 (conf G s) vs Ts'" |
|
162 |
apply (unfold widens_def) |
|
163 |
apply (rule list_all2_trans) |
|
164 |
apply auto |
|
165 |
done |
|
166 |
||
167 |
lemma conf_RefTD [rule_format (no_asm)]: |
|
168 |
"G,s\<turnstile>a'\<Colon>\<preceq>RefT T |
|
169 |
\<longrightarrow> a' = Null \<or> (\<exists>a obj T'. a' = Addr a \<and> heap s a = Some obj \<and> |
|
170 |
obj_ty obj = T' \<and> G\<turnstile>T'\<preceq>RefT T)" |
|
171 |
apply (unfold conf_def) |
|
172 |
apply (induct_tac "a'") |
|
173 |
apply (auto dest: widen_PrimT) |
|
174 |
done |
|
175 |
||
176 |
||
177 |
section "value list conformance" |
|
178 |
||
179 |
constdefs |
|
180 |
||
181 |
lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" |
|
182 |
("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70) |
|
183 |
"G,s\<turnstile>vs[\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<exists>v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T" |
|
184 |
||
185 |
lemma lconfD: "\<lbrakk>G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T\<rbrakk> \<Longrightarrow> G,s\<turnstile>(the (vs n))\<Colon>\<preceq>T" |
|
186 |
by (force simp: lconf_def) |
|
187 |
||
188 |
||
189 |
lemma lconf_cong [simp]: "\<And>s. G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L" |
|
190 |
by (auto simp: lconf_def) |
|
191 |
||
192 |
lemma lconf_lupd [simp]: "G,lupd(vn\<mapsto>v)s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L" |
|
193 |
by (auto simp: lconf_def) |
|
194 |
||
195 |
(* unused *) |
|
196 |
lemma lconf_new: "\<lbrakk>L vn = None; G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L" |
|
197 |
by (auto simp: lconf_def) |
|
198 |
||
199 |
lemma lconf_upd: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T; L vn = Some T\<rbrakk> \<Longrightarrow> |
|
200 |
G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L" |
|
201 |
by (auto simp: lconf_def) |
|
202 |
||
203 |
lemma lconf_ext: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> G,s\<turnstile>l(vn\<mapsto>v)[\<Colon>\<preceq>]L(vn\<mapsto>T)" |
|
204 |
by (auto simp: lconf_def) |
|
205 |
||
206 |
lemma lconf_map_sum [simp]: |
|
207 |
"G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 \<and> G,s\<turnstile>l2[\<Colon>\<preceq>]L2)" |
|
208 |
apply (unfold lconf_def) |
|
209 |
apply safe |
|
210 |
apply (case_tac [3] "n") |
|
211 |
apply (force split add: sum.split)+ |
|
212 |
done |
|
213 |
||
214 |
lemma lconf_ext_list [rule_format (no_asm)]: " |
|
215 |
\<And>X. \<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> |
|
12893 | 216 |
\<forall>vs Ts. distinct vns \<longrightarrow> length Ts = length vns |
12854 | 217 |
\<longrightarrow> list_all2 (conf G s) vs Ts \<longrightarrow> G,s\<turnstile>l(vns[\<mapsto>]vs)[\<Colon>\<preceq>]L(vns[\<mapsto>]Ts)" |
218 |
apply (unfold lconf_def) |
|
219 |
apply (induct_tac "vns") |
|
220 |
apply clarsimp |
|
221 |
apply clarsimp |
|
222 |
apply (frule list_all2_lengthD) |
|
223 |
apply clarsimp |
|
224 |
done |
|
225 |
||
226 |
||
227 |
lemma lconf_deallocL: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L(vn\<mapsto>T); L vn = None\<rbrakk> \<Longrightarrow> G,s\<turnstile>l[\<Colon>\<preceq>]L" |
|
228 |
apply (simp only: lconf_def) |
|
229 |
apply safe |
|
230 |
apply (drule spec) |
|
231 |
apply (drule ospec) |
|
232 |
apply auto |
|
233 |
done |
|
234 |
||
235 |
||
236 |
lemma lconf_gext [elim]: "\<lbrakk>G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s'\<rbrakk> \<Longrightarrow> G,s'\<turnstile>l[\<Colon>\<preceq>]L" |
|
237 |
apply (simp only: lconf_def) |
|
238 |
apply fast |
|
239 |
done |
|
240 |
||
241 |
lemma lconf_empty [simp, intro!]: "G,s\<turnstile>vs[\<Colon>\<preceq>]empty" |
|
242 |
apply (unfold lconf_def) |
|
243 |
apply force |
|
244 |
done |
|
245 |
||
246 |
lemma lconf_init_vals [intro!]: |
|
247 |
" \<forall>n. \<forall>T\<in>fs n:is_type G T \<Longrightarrow> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs" |
|
248 |
apply (unfold lconf_def) |
|
249 |
apply force |
|
250 |
done |
|
251 |
||
252 |
||
253 |
section "object conformance" |
|
254 |
||
255 |
constdefs |
|
256 |
||
257 |
oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_" [71,71,71,71] 70) |
|
258 |
"G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> |
|
259 |
(case r of |
|
260 |
Heap a \<Rightarrow> is_type G (obj_ty obj) |
|
261 |
| Stat C \<Rightarrow> True)" |
|
262 |
(* |
|
263 |
lemma oconf_def2: "G,s\<turnstile>\<lparr>tag=oi,values=fs\<rparr>\<Colon>\<preceq>\<surd>r = |
|
264 |
(G,s\<turnstile>fs[\<Colon>\<preceq>]var_tys G oi r \<and> |
|
265 |
(case r of Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>) | Stat C \<Rightarrow> True))" |
|
266 |
by (simp add: oconf_def Let_def) |
|
267 |
*) |
|
268 |
(* |
|
269 |
lemma oconf_def2: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r = |
|
270 |
(G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> |
|
271 |
(case r of Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> True))" |
|
272 |
by (simp add: oconf_def Let_def) |
|
273 |
*) |
|
274 |
lemma oconf_is_type: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Heap a \<Longrightarrow> is_type G (obj_ty obj)" |
|
275 |
by (auto simp: oconf_def Let_def) |
|
276 |
||
277 |
lemma oconf_lconf: "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<Longrightarrow> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r" |
|
278 |
by (simp add: oconf_def) |
|
279 |
||
280 |
lemma oconf_cong [simp]: "G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r" |
|
281 |
by (auto simp: oconf_def Let_def) |
|
282 |
||
283 |
lemma oconf_init_obj_lemma: |
|
284 |
"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (DeclConcepts.fields G C); |
|
285 |
\<And>C c f fld. \<lbrakk>class G C = Some c; |
|
286 |
table_of (DeclConcepts.fields G C) f = Some fld \<rbrakk> |
|
287 |
\<Longrightarrow> is_type G (type fld); |
|
288 |
(case r of |
|
289 |
Heap a \<Rightarrow> is_type G (obj_ty obj) |
|
290 |
| Stat C \<Rightarrow> is_class G C) |
|
291 |
\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj \<lparr>values:=init_vals (var_tys G (tag obj) r)\<rparr>\<Colon>\<preceq>\<surd>r" |
|
292 |
apply (auto simp add: oconf_def) |
|
293 |
apply (drule_tac var_tys_Some_eq [THEN iffD1]) |
|
294 |
defer |
|
295 |
apply (subst obj_ty_cong) |
|
296 |
apply(auto dest!: fields_table_SomeD obj_ty_CInst1 obj_ty_Arr1 |
|
297 |
split add: sum.split_asm obj_tag.split_asm) |
|
298 |
done |
|
299 |
||
300 |
(* |
|
301 |
lemma oconf_init_obj_lemma: |
|
302 |
"\<lbrakk>\<And>C c. class G C = Some c \<Longrightarrow> unique (fields G C); |
|
303 |
\<And>C c f fld. \<lbrakk>class G C = Some c; table_of (fields G C) f = Some fld \<rbrakk> |
|
304 |
\<Longrightarrow> is_type G (type fld); |
|
305 |
(case r of |
|
306 |
Heap a \<Rightarrow> is_type G (obj_ty \<lparr>tag=oi,values=fs\<rparr>) |
|
307 |
| Stat C \<Rightarrow> is_class G C) |
|
308 |
\<rbrakk> \<Longrightarrow> G,s\<turnstile>\<lparr>tag=oi, values=init_vals (var_tys G oi r)\<rparr>\<Colon>\<preceq>\<surd>r" |
|
309 |
apply (auto simp add: oconf_def) |
|
310 |
apply (drule_tac var_tys_Some_eq [THEN iffD1]) |
|
311 |
defer |
|
312 |
apply (subst obj_ty_eq) |
|
313 |
apply(auto dest!: fields_table_SomeD split add: sum.split_asm obj_tag.split_asm) |
|
314 |
done |
|
315 |
*) |
|
316 |
||
317 |
||
318 |
section "state conformance" |
|
319 |
||
320 |
constdefs |
|
321 |
||
322 |
conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool" ( "_\<Colon>\<preceq>_" [71,71] 70) |
|
323 |
"xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in |
|
324 |
(\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and> |
|
325 |
\<spacespace> G,s\<turnstile>l [\<Colon>\<preceq>]L\<spacespace> \<and> |
|
326 |
(\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable))" |
|
327 |
||
328 |
section "conforms" |
|
329 |
||
330 |
lemma conforms_globsD: |
|
331 |
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); globs s r = Some obj\<rbrakk> \<Longrightarrow> G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r" |
|
332 |
by (auto simp: conforms_def Let_def) |
|
333 |
||
334 |
lemma conforms_localD: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> G,s\<turnstile>locals s[\<Colon>\<preceq>]L" |
|
335 |
by (auto simp: conforms_def Let_def) |
|
336 |
||
337 |
lemma conforms_XcptLocD: "\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); x = Some (Xcpt (Loc a))\<rbrakk> \<Longrightarrow> |
|
338 |
G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)" |
|
339 |
by (auto simp: conforms_def Let_def) |
|
340 |
||
341 |
lemma conforms_RefTD: |
|
342 |
"\<lbrakk>G,s\<turnstile>a'\<Colon>\<preceq>RefT t; a' \<noteq> Null; (x,s) \<Colon>\<preceq>(G, L)\<rbrakk> \<Longrightarrow> |
|
343 |
\<exists>a obj. a' = Addr a \<and> globs s (Inl a) = Some obj \<and> |
|
344 |
G\<turnstile>obj_ty obj\<preceq>RefT t \<and> is_type G (obj_ty obj)" |
|
345 |
apply (drule_tac conf_RefTD) |
|
346 |
apply clarsimp |
|
347 |
apply (rule conforms_globsD [THEN oconf_is_type]) |
|
348 |
apply auto |
|
349 |
done |
|
350 |
||
351 |
lemma conforms_Jump [iff]: |
|
352 |
"((Some (Jump j), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))" |
|
353 |
by (auto simp: conforms_def) |
|
354 |
||
355 |
lemma conforms_StdXcpt [iff]: |
|
356 |
"((Some (Xcpt (Std xn)), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))" |
|
357 |
by (auto simp: conforms_def) |
|
358 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
359 |
lemma conforms_Err [iff]: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
360 |
"((Some (Error e), s)\<Colon>\<preceq>(G, L)) = (Norm s\<Colon>\<preceq>(G, L))" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
361 |
by (auto simp: conforms_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
362 |
|
12854 | 363 |
lemma conforms_raise_if [iff]: |
364 |
"((raise_if c xn x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))" |
|
365 |
by (auto simp: abrupt_if_def) |
|
366 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
367 |
lemma conforms_error_if [iff]: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
368 |
"((error_if c err x, s)\<Colon>\<preceq>(G, L)) = ((x, s)\<Colon>\<preceq>(G, L))" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
369 |
by (auto simp: abrupt_if_def split: split_if) |
12854 | 370 |
|
371 |
lemma conforms_NormI: "(x, s)\<Colon>\<preceq>(G, L) \<Longrightarrow> Norm s\<Colon>\<preceq>(G, L)" |
|
372 |
by (auto simp: conforms_def Let_def) |
|
373 |
||
374 |
lemma conforms_absorb [rule_format]: |
|
375 |
"(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)" |
|
376 |
apply (rule impI) |
|
377 |
apply ( case_tac a) |
|
378 |
apply (case_tac "absorb j a") |
|
379 |
apply auto |
|
380 |
apply (case_tac "absorb j (Some a)",auto) |
|
381 |
apply (erule conforms_NormI) |
|
382 |
done |
|
383 |
||
384 |
lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; |
|
385 |
G,s\<turnstile>locals s[\<Colon>\<preceq>]L; |
|
386 |
\<forall>a. x = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow> |
|
387 |
(x, s)\<Colon>\<preceq>(G, L)" |
|
388 |
by (auto simp: conforms_def Let_def) |
|
389 |
||
390 |
lemma conforms_xconf: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); |
|
391 |
\<forall>a. x' = Some (Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)\<rbrakk> \<Longrightarrow> |
|
392 |
(x',s)\<Colon>\<preceq>(G,L)" |
|
393 |
by (fast intro: conformsI elim: conforms_globsD conforms_localD) |
|
394 |
||
395 |
lemma conforms_lupd: |
|
396 |
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); L vn = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L)" |
|
397 |
by (force intro: conformsI lconf_upd dest: conforms_globsD conforms_localD |
|
398 |
conforms_XcptLocD simp: oconf_def) |
|
399 |
||
400 |
||
401 |
lemmas conforms_allocL_aux = conforms_localD [THEN lconf_ext] |
|
402 |
||
403 |
lemma conforms_allocL: |
|
404 |
"\<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x, lupd(vn\<mapsto>v)s)\<Colon>\<preceq>(G, L(vn\<mapsto>T))" |
|
405 |
by (force intro: conformsI dest: conforms_globsD |
|
406 |
elim: conforms_XcptLocD conforms_allocL_aux simp: oconf_def) |
|
407 |
||
408 |
lemmas conforms_deallocL_aux = conforms_localD [THEN lconf_deallocL] |
|
409 |
||
410 |
lemma conforms_deallocL: "\<And>s.\<lbrakk>s\<Colon>\<preceq>(G, L(vn\<mapsto>T)); L vn = None\<rbrakk> \<Longrightarrow> s\<Colon>\<preceq>(G,L)" |
|
411 |
by (fast intro: conformsI dest: conforms_globsD |
|
412 |
elim: conforms_XcptLocD conforms_deallocL_aux) |
|
413 |
||
414 |
lemma conforms_gext: "\<lbrakk>(x, s)\<Colon>\<preceq>(G,L); s\<le>|s'; |
|
415 |
\<forall>r. \<forall>obj\<in>globs s' r: G,s'\<turnstile>obj\<Colon>\<preceq>\<surd>r; |
|
416 |
locals s'=locals s\<rbrakk> \<Longrightarrow> (x,s')\<Colon>\<preceq>(G,L)" |
|
417 |
by (force intro!: conformsI dest: conforms_localD conforms_XcptLocD) |
|
418 |
||
419 |
||
420 |
lemma conforms_xgext: |
|
421 |
"\<lbrakk>(x ,s)\<Colon>\<preceq>(G,L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s\<rbrakk> \<Longrightarrow> (x',s)\<Colon>\<preceq>(G,L)" |
|
422 |
apply (erule_tac conforms_xconf) |
|
423 |
apply (fast dest: conforms_XcptLocD) |
|
424 |
done |
|
425 |
||
426 |
lemma conforms_gupd: "\<And>obj. \<lbrakk>(x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; s\<le>|gupd(r\<mapsto>obj)s\<rbrakk> |
|
427 |
\<Longrightarrow> (x, gupd(r\<mapsto>obj)s)\<Colon>\<preceq>(G, L)" |
|
428 |
apply (rule conforms_gext) |
|
429 |
apply auto |
|
430 |
apply (force dest: conforms_globsD simp add: oconf_def)+ |
|
431 |
done |
|
432 |
||
433 |
lemma conforms_upd_gobj: "\<lbrakk>(x,s)\<Colon>\<preceq>(G, L); globs s r = Some obj; |
|
434 |
var_tys G (tag obj) r n = Some T; G,s\<turnstile>v\<Colon>\<preceq>T\<rbrakk> \<Longrightarrow> (x,upd_gobj r n v s)\<Colon>\<preceq>(G,L)" |
|
435 |
apply (rule conforms_gext) |
|
436 |
apply auto |
|
437 |
apply (drule (1) conforms_globsD) |
|
438 |
apply (simp add: oconf_def) |
|
439 |
apply safe |
|
440 |
apply (rule lconf_upd) |
|
441 |
apply auto |
|
442 |
apply (simp only: obj_ty_cong) |
|
443 |
apply (force dest: conforms_globsD intro!: lconf_upd |
|
444 |
simp add: oconf_def cong del: sum.weak_case_cong) |
|
445 |
done |
|
446 |
||
447 |
lemma conforms_set_locals: |
|
448 |
"\<lbrakk>(x,s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<Colon>\<preceq>]L\<rbrakk> \<Longrightarrow> (x,set_locals l s)\<Colon>\<preceq>(G,L)" |
|
449 |
apply (auto intro!: conformsI dest: conforms_globsD |
|
450 |
elim!: conforms_XcptLocD simp add: oconf_def) |
|
451 |
done |
|
452 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
453 |
lemma conforms_locals [rule_format]: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
454 |
"(a,b)\<Colon>\<preceq>(G, L) \<longrightarrow> L x = Some T \<longrightarrow> G,b\<turnstile>the (locals b x)\<Colon>\<preceq>T" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
455 |
apply (force simp: conforms_def Let_def lconf_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
456 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
457 |
|
12854 | 458 |
lemma conforms_return: "\<And>s'. \<lbrakk>(x,s)\<Colon>\<preceq>(G, L); (x',s')\<Colon>\<preceq>(G, L'); s\<le>|s'\<rbrakk> \<Longrightarrow> |
459 |
(x',set_locals (locals s) s')\<Colon>\<preceq>(G, L)" |
|
460 |
apply (rule conforms_xconf) |
|
461 |
prefer 2 apply (force dest: conforms_XcptLocD) |
|
462 |
apply (erule conforms_gext) |
|
463 |
apply (force dest: conforms_globsD)+ |
|
464 |
done |
|
465 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
466 |
|
12854 | 467 |
end |