equal
deleted
inserted
replaced
20 |
20 |
21 |
21 |
22 section "extension of global store" |
22 section "extension of global store" |
23 |
23 |
24 |
24 |
25 constdefs |
25 definition gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_" [71,71] 70) where |
26 |
|
27 gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_" [71,71] 70) |
|
28 "s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj" |
26 "s\<le>|s' \<equiv> \<forall>r. \<forall>obj\<in>globs s r: \<exists>obj'\<in>globs s' r: tag obj'= tag obj" |
29 |
27 |
30 text {* For the the proof of type soundness we will need the |
28 text {* For the the proof of type soundness we will need the |
31 property that during execution, objects are not lost and moreover retain the |
29 property that during execution, objects are not lost and moreover retain the |
32 values of their tags. So the object store grows conservatively. Note that if |
30 values of their tags. So the object store grows conservatively. Note that if |
96 done |
94 done |
97 |
95 |
98 |
96 |
99 section "value conformance" |
97 section "value conformance" |
100 |
98 |
101 constdefs |
99 definition conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_" [71,71,71,71] 70) where |
102 |
|
103 conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_" [71,71,71,71] 70) |
|
104 "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" |
100 "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" |
105 |
101 |
106 lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T" |
102 lemma conf_cong [simp]: "G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T" |
107 by (auto simp: conf_def) |
103 by (auto simp: conf_def) |
108 |
104 |
179 done |
175 done |
180 |
176 |
181 |
177 |
182 section "value list conformance" |
178 section "value list conformance" |
183 |
179 |
184 constdefs |
180 definition lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70) where |
185 |
|
186 lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" |
|
187 ("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70) |
|
188 "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" |
181 "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" |
189 |
182 |
190 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" |
183 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" |
191 by (force simp: lconf_def) |
184 by (force simp: lconf_def) |
192 |
185 |
265 defined values are of the right type, and not also that the value |
258 defined values are of the right type, and not also that the value |
266 is defined. |
259 is defined. |
267 *} |
260 *} |
268 |
261 |
269 |
262 |
270 constdefs |
263 definition wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70) where |
271 |
|
272 wlconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool" |
|
273 ("_,_\<turnstile>_[\<sim>\<Colon>\<preceq>]_" [71,71,71,71] 70) |
|
274 "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T" |
264 "G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts \<equiv> \<forall>n. \<forall>T\<in>Ts n: \<forall> v\<in>vs n: G,s\<turnstile>v\<Colon>\<preceq>T" |
275 |
265 |
276 lemma wlconfD: "\<lbrakk>G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts; Ts n = Some T; vs n = Some v\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T" |
266 lemma wlconfD: "\<lbrakk>G,s\<turnstile>vs[\<sim>\<Colon>\<preceq>]Ts; Ts n = Some T; vs n = Some v\<rbrakk> \<Longrightarrow> G,s\<turnstile>v\<Colon>\<preceq>T" |
277 by (auto simp: wlconf_def) |
267 by (auto simp: wlconf_def) |
278 |
268 |
346 "G,s\<turnstile>l[\<Colon>\<preceq>]L \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L" |
336 "G,s\<turnstile>l[\<Colon>\<preceq>]L \<Longrightarrow> G,s\<turnstile>l[\<sim>\<Colon>\<preceq>]L" |
347 by (force simp add: lconf_def wlconf_def) |
337 by (force simp add: lconf_def wlconf_def) |
348 |
338 |
349 section "object conformance" |
339 section "object conformance" |
350 |
340 |
351 constdefs |
341 definition oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_" [71,71,71,71] 70) where |
352 |
|
353 oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_" [71,71,71,71] 70) |
|
354 "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> |
342 "G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>values obj[\<Colon>\<preceq>]var_tys G (tag obj) r \<and> |
355 (case r of |
343 (case r of |
356 Heap a \<Rightarrow> is_type G (obj_ty obj) |
344 Heap a \<Rightarrow> is_type G (obj_ty obj) |
357 | Stat C \<Rightarrow> True)" |
345 | Stat C \<Rightarrow> True)" |
358 |
346 |
383 split add: sum.split_asm obj_tag.split_asm) |
371 split add: sum.split_asm obj_tag.split_asm) |
384 done |
372 done |
385 |
373 |
386 section "state conformance" |
374 section "state conformance" |
387 |
375 |
388 constdefs |
376 definition conforms :: "state \<Rightarrow> env' \<Rightarrow> bool" ("_\<Colon>\<preceq>_" [71,71] 70) where |
389 |
|
390 conforms :: "state \<Rightarrow> env' \<Rightarrow> bool" ( "_\<Colon>\<preceq>_" [71,71] 70) |
|
391 "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in |
377 "xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in |
392 (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and> |
378 (\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and> |
393 \<spacespace> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and> |
379 \<spacespace> G,s\<turnstile>l [\<sim>\<Colon>\<preceq>]L\<spacespace> \<and> |
394 (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and> |
380 (\<forall>a. fst xs=Some(Xcpt (Loc a)) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq> Class (SXcpt Throwable)) \<and> |
395 (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None)" |
381 (fst xs=Some(Jump Ret) \<longrightarrow> l Result \<noteq> None)" |