Up to index of Isabelle/Bali5
theory Conform = State(* Title: isabelle/Bali/Conform.thy
ID: $Id: Conform.thy,v 1.5 2000/10/19 21:21:51 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Conformance notions for the type soundness proof for Java
design issues:
* lconf allows for (arbitrary) inaccessible values
* "conforms" does not directly imply that the dynamic types of all objects on
the heap are indeed existing classes. Yet this can be inferred for all
referenced objs.
*)
Conform = State +
types env_ = "prog × (lname, ty) table" (* same as env of WellType.thy *)
constdefs
gext :: "st \<Rightarrow> st \<Rightarrow> bool" ("_\<le>|_" [71,71] 70)
"s\<le>|s' \<equiv> \<forall>r. \<forall>(oi, fs)\<in>globs s r: \<exists>(oi',fs')\<in>globs s' r: oi' = oi"
conf :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>_" [71,71,71,71] 70)
"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"
lconf :: "prog \<Rightarrow> st \<Rightarrow> ('a, val) table \<Rightarrow> ('a, ty) table \<Rightarrow> bool"
("_,_\<turnstile>_[\<Colon>\<preceq>]_" [71,71,71,71] 70)
"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"
oconf :: "prog \<Rightarrow> st \<Rightarrow> obj \<Rightarrow> oref \<Rightarrow> bool" ("_,_\<turnstile>_\<Colon>\<preceq>\<surd>_" [71,71,71,71] 70)
"G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r \<equiv> G,s\<turnstile>snd obj[\<Colon>\<preceq>]var_tys G (fst obj) r \<and> (case r of
Heap a \<Rightarrow> is_type G (obj_ty obj) | Stat C \<Rightarrow> True)"
conforms :: "state \<Rightarrow> env_ \<Rightarrow> bool" ( "_\<Colon>\<preceq>_" [71,71] 70)
"xs\<Colon>\<preceq>E \<equiv> let (G, L) = E; s = snd xs; l = locals s in
(\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj \<Colon>\<preceq>\<surd>r) \<and>
G,s\<turnstile>l [\<Colon>\<preceq>]L \<and>
(\<forall>a. fst xs=Some(XcptLoc a) \<longrightarrow> G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable))"
end
theorem gext_objD:
[| s\<le>|s'; globs s r = Some (oi, fs) |] ==> EX fs'. globs s' r = Some (oi, fs')
theorem rev_gext_objD:
[| globs s r = Some (oi, fs); s\<le>|s' |] ==> EX fs'. globs s' r = Some (oi, fs')
theorem init_class_obj_inited:
(init_class_obj G C) s1\<le>|s2 ==> inited C (globs s2)
theorem gext_refl:
s\<le>|s
theorem gext_gupd:
globs s r = None ==> s\<le>|gupd(r\<mapsto>x) s
theorem gext_new:
globs s r = None ==> s\<le>|init_obj G oi r s
theorem gext_trans:
[| s\<le>|s'; s'\<le>|s'' |] ==> s\<le>|s''
theorem gext_upd_gobj:
s\<le>|upd_gobj r n v s
theorem gext_cong1:
set_locals l s1\<le>|s2 = s1\<le>|s2
theorem gext_cong2:
s1\<le>|set_locals l s2 = s1\<le>|s2
theorem gext_lupd1:
lupd(vn\<mapsto>v) s1\<le>|s2 = s1\<le>|s2
theorem gext_lupd2:
s1\<le>|lupd(vn\<mapsto>v) s2 = s1\<le>|s2
theorem inited_gext:
[| inited C (globs s); s\<le>|s' |] ==> inited C (globs s')
theorem conf_cong:
G,set_locals l s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T
theorem conf_lupd:
G,lupd(vn\<mapsto>va) s\<turnstile>v\<Colon>\<preceq>T = G,s\<turnstile>v\<Colon>\<preceq>T
theorem conf_PrimT:
ALL dt. typeof dt v = Some (PrimT t) ==> G,s\<turnstile>v\<Colon>\<preceq>PrimT t
theorem conf_litval:
typeof (%a. None) v = Some T ==> G,s\<turnstile>v\<Colon>\<preceq>T
theorem conf_Null:
G,s\<turnstile>Null\<Colon>\<preceq>T = G|-NT<=:T
theorem conf_Addr:
G,s\<turnstile>Addr a\<Colon>\<preceq>T = (EX obj. heap s a = Some obj & G|-obj_ty obj<=:T)
theorem defval_conf:
is_type G T ==> G,s\<turnstile>default_val T\<Colon>\<preceq>T
theorem conf_widen:
[| G|-T<=:T'; G,s\<turnstile>x\<Colon>\<preceq>T; ws_prog G |] ==> G,s\<turnstile>x\<Colon>\<preceq>T'
theorem conf_gext:
[| G,s\<turnstile>v\<Colon>\<preceq>T; s\<le>|s' |] ==> G,s'\<turnstile>v\<Colon>\<preceq>T
theorem conf_list_widen:
[| ws_prog G; list_all2 (conf G s) vs Ts; G\<turnstile>Ts[\<preceq>]Ts' |] ==> list_all2 (conf G s) vs Ts'
theorem conf_RefTD:
G,s\<turnstile>a'\<Colon>\<preceq>RefT T
==> a' = Null |
(EX a oi vs T'.
a' = Addr a &
heap s a = Some (oi, vs) & obj_ty (oi, vs) = T' & G|-T'<=:RefT T)
theorem lconfD:
[| G,s\<turnstile>vs[\<Colon>\<preceq>]Ts; Ts n = Some T |] ==> G,s\<turnstile>the (vs n)\<Colon>\<preceq>T
theorem lconf_cong:
G,set_locals x s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L
theorem lconf_lupd:
G,lupd(vn\<mapsto>v) s\<turnstile>l[\<Colon>\<preceq>]L = G,s\<turnstile>l[\<Colon>\<preceq>]L
theorem lconf_new:
[| L vn = None; G,s\<turnstile>l[\<Colon>\<preceq>]L |] ==> G,s\<turnstile>l(vn|->v)[\<Colon>\<preceq>]L
theorem lconf_upd:
[| G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T;
L vn = Some T |]
==> G,s\<turnstile>l(vn|->v)[\<Colon>\<preceq>]L
theorem lconf_ext:
[| G,s\<turnstile>l[\<Colon>\<preceq>]L; G,s\<turnstile>v\<Colon>\<preceq>T |] ==> G,s\<turnstile>l(vn|->v)[\<Colon>\<preceq>]L(vn|->T)
theorem lconf_map_sum:
G,s\<turnstile>l1 (+) l2[\<Colon>\<preceq>]L1 (+) L2 = (G,s\<turnstile>l1[\<Colon>\<preceq>]L1 & G,s\<turnstile>l2[\<Colon>\<preceq>]L2)
theorem lconf_ext_list:
[| G,s\<turnstile>l[\<Colon>\<preceq>]L; nodups vns; length Ts = length vns;
list_all2 (conf G s) vs Ts |]
==> G,s\<turnstile>l(vns[|->]vs)[\<Colon>\<preceq>]L(vns[|->]Ts)
theorem lconf_deallocL:
[| G,s\<turnstile>l[\<Colon>\<preceq>]L(vn|->T); L vn = None |] ==> G,s\<turnstile>l[\<Colon>\<preceq>]L
theorem lconf_gext:
[| G,s\<turnstile>l[\<Colon>\<preceq>]L; s\<le>|s' |] ==> G,s'\<turnstile>l[\<Colon>\<preceq>]L
theorem lconf_empty:
G,s\<turnstile>vs[\<Colon>\<preceq>]empty
theorem lconf_init_vals:
ALL n. Ball (o2s (fs n)) (is_type G) ==> G,s\<turnstile>init_vals fs[\<Colon>\<preceq>]fs
theorem oconf_def2:
G,s\<turnstile>(oi, fs)\<Colon>\<preceq>\<surd>r = (G,s\<turnstile>fs[\<Colon>\<preceq>]var_tys G oi r & (case r of Inl a => is_type G (obj_ty (oi, fs)) | Inr C => True))
theorem oconf_is_type:
G,s\<turnstile>obj\<Colon>\<preceq>\<surd>Inl a ==> is_type G (obj_ty obj)
theorem oconf_cong:
G,set_locals l s\<turnstile>obj\<Colon>\<preceq>\<surd>r = G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r
theorem oconf_init_obj_lemma:
[| !!C c. class G C = Some c ==> unique (fields G C);
!!C c f m T.
[| class G C = Some c; table_of (fields G C) f = Some (m, T) |]
==> is_type G T;
case r of Inl a => is_type G (obj_ty (oi, fs)) | Inr C => is_class G C |]
==> G,s\<turnstile>(oi, init_vals (var_tys G oi r))\<Colon>\<preceq>\<surd>r
theorem conforms_globsD:
[| (x, s)\<Colon>\<preceq>(G, L); globs s r = Some (oi, fs) |] ==> G,s\<turnstile>(oi, fs)\<Colon>\<preceq>\<surd>r
theorem conforms_localD:
(x, s)\<Colon>\<preceq>(G, L) ==> G,s\<turnstile>locals s[\<Colon>\<preceq>]L
theorem conforms_XcptLocD:
[| (x, s)\<Colon>\<preceq>(G, L); x = Some (XcptLoc a) |] ==> G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable)
theorem conforms_RefTD:
[| G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; a' ~= Null;
(x2, s2)\<Colon>\<preceq>(G, L) |]
==> EX a oi vs.
a' = Addr a &
globs s2 (Inl a) = Some (oi, vs) &
G|-obj_ty (oi, vs)<=:RefT t & is_type G (obj_ty (oi, vs))
theorem conforms_StdXcpt:
(Some (StdXcpt xn), s)\<Colon>\<preceq>(G, L) = Norm s\<Colon>\<preceq>(G, L)
theorem conforms_raise_if:
((raise_if c xn) x, s)\<Colon>\<preceq>(G, L) = (x, s)\<Colon>\<preceq>(G, L)
theorem conforms_NormI:
(x, s)\<Colon>\<preceq>(G, L) ==> Norm s\<Colon>\<preceq>(G, L)
theorem conformsI:
[| ALL r. ! (oi, fs):globs s r:
G,s\<turnstile>(oi, fs)\<Colon>\<preceq>\<surd>r;
G,s\<turnstile>locals s[\<Colon>\<preceq>]L;
ALL a. x = Some (XcptLoc a) -->
G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable) |]
==> (x, s)\<Colon>\<preceq>(G, L)
theorem conforms_xconf:
[| (x, s)\<Colon>\<preceq>(G, L);
ALL a. x' = Some (XcptLoc a) -->
G,s\<turnstile>Addr a\<Colon>\<preceq>Class (SXcpt Throwable) |]
==> (x', s)\<Colon>\<preceq>(G, L)
theorem conforms_lupd:
[| (x, s)\<Colon>\<preceq>(G, L); L vn = Some T;
G,s\<turnstile>v\<Colon>\<preceq>T |]
==> (x, lupd(vn\<mapsto>v) s)\<Colon>\<preceq>(G, L)
theorem conforms_allocL:
[| (x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>v\<Colon>\<preceq>T |] ==> (x, lupd(vn\<mapsto>v) s)\<Colon>\<preceq>(G, L(vn|->T))
theorem conforms_deallocL:
[| s\<Colon>\<preceq>(G, L(vn|->T)); L vn = None |] ==> s\<Colon>\<preceq>(G, L)
theorem conforms_gext:
[| (x, s)\<Colon>\<preceq>(G, L); s\<le>|s';
ALL r. ! (oi, fs):globs s' r:
G,s'\<turnstile>(oi, fs)\<Colon>\<preceq>\<surd>r;
locals s' = locals s |]
==> (x, s')\<Colon>\<preceq>(G, L)
theorem conforms_xgext:
[| (x, s)\<Colon>\<preceq>(G, L); (x', s')\<Colon>\<preceq>(G, L); s'\<le>|s |] ==> (x', s)\<Colon>\<preceq>(G, L)
theorem conforms_gupd:
[| (x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r;
s\<le>|gupd(r\<mapsto>obj) s |]
==> (x, gupd(r\<mapsto>obj) s)\<Colon>\<preceq>(G, L)
theorem conforms_upd_gobj:
[| (x, s)\<Colon>\<preceq>(G, L); globs s r = Some (oi, vs);
var_tys G oi r n = Some T; G,s\<turnstile>v\<Colon>\<preceq>T |]
==> (x, upd_gobj r n v s)\<Colon>\<preceq>(G, L)
theorem conforms_set_locals:
[| (x, s)\<Colon>\<preceq>(G, L'); G,s\<turnstile>l[\<Colon>\<preceq>]L |] ==> (x, set_locals l s)\<Colon>\<preceq>(G, L)
theorem conforms_return:
[| (x, s)\<Colon>\<preceq>(G, L); (x', s')\<Colon>\<preceq>(G, L'); s\<le>|s' |] ==> (x', set_locals (locals s) s')\<Colon>\<preceq>(G, L)