Up to index of Isabelle/Bali5
theory TypeSafe = Eval + WellForm + Conform(* Title: isabelle/Bali/TypeSafe.thy
ID: $Id: TypeSafe.thy,v 1.22 2000/11/28 23:06:20 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
The type soundness proof for Java
*)
TypeSafe = Eval + WellForm + Conform +
constdefs
DynT_prop::"[prog,inv_mode,tname,ref_ty] \<Rightarrow> bool" ("_\<turnstile>_\<rightarrow>_\<preceq>_"[71,71,71,71]70)
"G\<turnstile>mode\<rightarrow>D\<preceq>t \<equiv> mode = IntVir \<longrightarrow> is_class G D \<and>
(if (\<exists>T. t=ArrayT T) then D=Object else G\<turnstile>Class D\<preceq>RefT t)"
assign_conforms :: "st \<Rightarrow> (val \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> ty \<Rightarrow> env \<Rightarrow> bool"
("_\<le>|_\<preceq>_\<Colon>\<preceq>_" [71,71,71,71] 70)
"s\<le>|f\<preceq>T\<Colon>\<preceq>E \<equiv>
\<forall>s' w. Norm s'\<Colon>\<preceq>E \<longrightarrow> fst E,s'\<turnstile>w\<Colon>\<preceq>T \<longrightarrow> s\<le>|s' \<longrightarrow> assign f w (Norm s')\<Colon>\<preceq>E"
rconf :: "prog \<Rightarrow> lenv \<Rightarrow> st \<Rightarrow> term \<Rightarrow> vals \<Rightarrow> tys \<Rightarrow> bool"
("_,_,_\<turnstile>_\<succ>_\<Colon>\<preceq>_" [71,71,71,71,71,71] 70)
"G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T \<equiv> case T of
Inl T \<Rightarrow> if (\<exists>vf. t=In2 vf)
then G,s\<turnstile>fst (the_In2 v)\<Colon>\<preceq>T \<and> s\<le>|snd (the_In2 v)\<preceq>T\<Colon>\<preceq>(G,L)
else G,s\<turnstile>the_In1 v\<Colon>\<preceq>T
| Inr Ts \<Rightarrow> list_all2 (conf G s) (the_In3 v) Ts"
end
theorem rconf_In1:
G,L,s\<turnstile>In1 ec\<succ>In1 v\<Colon>\<preceq>Inl T = G,s\<turnstile>v\<Colon>\<preceq>T
theorem rconf_In2:
G,L,s\<turnstile>In2 va\<succ>In2 vf\<Colon>\<preceq>Inl T = (G,s\<turnstile>fst vf\<Colon>\<preceq>T & s\<le>|snd vf\<preceq>T\<Colon>\<preceq>(G, L))
theorem rconf_In3:
G,L,s\<turnstile>In3 es\<succ>In3 vs\<Colon>\<preceq>Inr Ts = list_all2 (conf G s) vs Ts
theorem conf_fits:
G,s\<turnstile>v\<Colon>\<preceq>T ==> G,s\<turnstile>v fits T
theorem fits_conf:
[| G,s\<turnstile>v\<Colon>\<preceq>T; G|-T<=:? T'; G,s\<turnstile>v fits T';
ws_prog G |]
==> G,s\<turnstile>v\<Colon>\<preceq>T'
theorem fits_Array:
[| G,s\<turnstile>v\<Colon>\<preceq>T; G|-T'.[]<=:T.[];
G,s\<turnstile>v fits T'; ws_prog G |]
==> G,s\<turnstile>v\<Colon>\<preceq>T'
theorem halloc_gext:
G|-s1 -halloc oi>a-> s2 ==> snd s1\<le>|snd s2
theorem sxalloc_gext:
G|-s1 -sxalloc-> s2 ==> snd s1\<le>|snd s2
theorem eval_gext_lemma:
G|-s -t>-> (w, s')
==> snd s\<le>|snd s' &
(case w of In1 v => True
| In2 vf => normal s --> (ALL v x s. s\<le>|snd (assign (snd vf) v (x, s)))
| In3 vs => True)
theorem evar_gext_f:
G|-Norm s1 -e=>vf-> s2 ==> s\<le>|snd (assign (snd vf) v (x, s))
theorem eval_gext':
G|-(x1, s1) -t>-> (w, x2, s2) ==> s1\<le>|s2
theorem init_yields_initd:
G|-Norm s1 -init C-> s2 ==> initd C s2 [!]
theorem oconf_init_obj:
[| wf_prog G;
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_newG:
[| globs s oref = None; (x, s)\<Colon>\<preceq>(G, L); wf_prog G;
case oref of Inl a => is_type G (obj_ty (oi, fs)) | Inr C => is_class G C |]
==> (x, init_obj G oi oref s)\<Colon>\<preceq>(G, L)
theorem conforms_init_class_obj:
[| (x, s)\<Colon>\<preceq>(G, L); wf_prog G; class G C = Some y;
¬ inited C (globs s) |]
==> (x, (init_class_obj G C) s)\<Colon>\<preceq>(G, L)
theorem fst_init_lvars:
fst (init_lvars G C sig (invmode m e) a' pvs (x, s)) = (if m then x else (np a') x)
theorem halloc_conforms:
[| G|-s1 -halloc oi>a-> s2; wf_prog G; s1\<Colon>\<preceq>(G, L);
is_type G (obj_ty (oi, fs)) |]
==> s2\<Colon>\<preceq>(G, L)
[!]
theorem halloc_type_sound:
[| G|-s1 -halloc oi>a-> s2; wf_prog G; s1\<Colon>\<preceq>(G, L);
T = obj_ty (oi, fs); is_type G T |]
==> s2\<Colon>\<preceq>(G, L) &
(%(x', s'). x' = None --> G,s'\<turnstile>Addr a\<Colon>\<preceq>T) s2
[!]
theorem sxalloc_type_sound:
[| G|-s1 -sxalloc-> s2; wf_prog G |]
==> case fst s1 of None => s2 = s1
| Some x =>
EX a. fst s2 = Some (XcptLoc a) &
(ALL L. s1\<Colon>\<preceq>(G, L) --> s2\<Colon>\<preceq>(G, L))
[!]
theorem wt_init_comp_ty:
is_type G T ==> (G, L)|-init_comp_ty T:<> [!]
theorem DynT_propI:
[| (x, s)\<Colon>\<preceq>(G, L); G,s\<turnstile>a'\<Colon>\<preceq>RefT t;
wf_prog G; mode = IntVir --> a' ~= Null |]
==> G\<turnstile>mode\<rightarrow>target mode s a' cT\<preceq>t
theorem DynT_mheadsD:
[| the (cmethd G dynT sig) = (md, (m', pns, rT), lvars, bdy);
G\<turnstile>invmode m e\<rightarrow>dynT\<preceq>t; wf_prog G;
(G, L)|-e:-RefT t; (cT, m, pnsa, T) : mheads G t sig;
target (invmode m e) s2 a' cT = dynT |]
==> cmethd G dynT sig = Some (md, (m, pns, rT), lvars, bdy) &
G|-rT<=:T &
m' = m &
wf_mdecl G md (sig, (m, pns, rT), lvars, bdy) &
is_class G dynT &
G|-dynT<=:C md &
is_class G md &
(invmode m e ~= IntVir -->
(EX C. t = ClassT C & G|-C<=:C md) & cT = ClassT md)
[!]
theorem DynT_conf:
[| G|-target mode s2 a' cT<=:C md; wf_prog G;
G,s2\<turnstile>a'\<Colon>\<preceq>RefT t; mode = IntVir --> a' ~= Null;
mode ~= IntVir --> (EX C. t = ClassT C & G|-C<=:C md) & cT = ClassT md |]
==> G,s2\<turnstile>a'\<Colon>\<preceq>Class md
theorem Ass_lemma:
[| G|-Norm s0 -va=>(w, f)-> Norm s1; G|-Norm s1 -e->v-> Norm s2;
G,s2\<turnstile>v\<Colon>\<preceq>T';
s1\<le>|s2 --> assign f v (Norm s2)\<Colon>\<preceq>(G, L) |]
==> assign f v (Norm s2)\<Colon>\<preceq>(G, L) &
(%(x', s'). x' = None --> G,s'\<turnstile>v\<Colon>\<preceq>T')
(assign f v (Norm s2))
theorem Throw_lemma:
[| G|-tn<=:C SXcpt Throwable; wf_prog G; (x1, s1)\<Colon>\<preceq>(G, L);
x1 = None --> G,s1\<turnstile>a'\<Colon>\<preceq>Class tn |]
==> xupd (throw a') (x1, s1)\<Colon>\<preceq>(G, L)
theorem Try_lemma:
[| G|-obj_ty (the (globs s1' (Inl a)))<=:Class tn;
(Some (XcptLoc a), s1')\<Colon>\<preceq>(G, L); wf_prog G |]
==> Norm (lupd(vn\<mapsto>Addr a) s1')\<Colon>\<preceq>(G, L(vn|->Class tn))
theorem Fin_lemma:
[| G|-Norm s1 -c2-> s2; wf_prog G; (x1, s1)\<Colon>\<preceq>(G, L);
s2\<Colon>\<preceq>(G, L) |]
==> xupd (xcpt_if (EX y. x1 = Some y) x1) s2\<Colon>\<preceq>(G, L)
theorem FVar_lemma1:
[| table_of (fields G Ca) (fn, C) = Some (stat, fT);
x2 = None --> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; wf_prog G;
class G Ca = Some y; G|-Ca<=:C C; C ~= Object; class G C = Some ya;
(x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2; inited C (globs s1);
(if stat then id else np a) x2 = None |]
==> EX oi fs.
globs s2 (if stat then Inr C else Inl (the_Addr a)) = Some (oi, fs) &
var_tys G oi (if stat then Inr C else Inl (the_Addr a)) (Inl (fn, C)) =
Some fT
theorem FVar_lemma:
[| (v, Norm s2') = fvar C stat fn a (x2, s2); class G Ca = Some y; G|-Ca<=:C C;
table_of (fields G Ca) (fn, C) = Some (stat, fT); wf_prog G;
x2 = None --> G,s2\<turnstile>a\<Colon>\<preceq>Class Ca; C ~= Object;
class G C = Some ya; (x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2;
inited C (globs s1) |]
==> G,s2'\<turnstile>fst v\<Colon>\<preceq>fT &
s2'\<le>|snd v\<preceq>fT\<Colon>\<preceq>(G, L)
theorem AVar_lemma1:
[| globs s2 (Inl a) = Some (Arr ty i, vs); the_Intg i' in_bounds i; wf_prog G;
G|-ty.[]<=:Tb.[]; Norm s2\<Colon>\<preceq>(G, L) |]
==> G,s2\<turnstile>the (vs (Inr (the_Intg i')))\<Colon>\<preceq>Tb
theorem AVar_lemma:
[| wf_prog G; G|-(x1, s1) -e2->i-> (x2, s2);
(v, Norm s2') = avar G i a (x2, s2);
x1 = None --> G,s1\<turnstile>a\<Colon>\<preceq>Ta.[];
(x2, s2)\<Colon>\<preceq>(G, L); s1\<le>|s2 |]
==> G,s2'\<turnstile>fst v\<Colon>\<preceq>Ta &
s2'\<le>|snd v\<preceq>Ta\<Colon>\<preceq>(G, L)
theorem conforms_init_lvars_lemma:
[| wf_prog G; wf_mhead G (mn, pTs) (m, pns, rT);
Ball (set lvars) (split (%vn. is_type G)); list_all2 (conf G s2) pvs pTsa;
G\<turnstile>pTsa[\<preceq>]pTs |]
==> G,s2\<turnstile>init_vals (table_of lvars)(pns[|->]pvs
)[\<Colon>\<preceq>]table_of lvars(pns[|->]pTs)
theorem conforms_init_lvars:
[| wf_mhead G (mn, pTs) (m, pns', rT'); wf_prog G;
Ball (set lvars) (split (%vn. is_type G)); list_all2 (conf G s2) pvs pTsa;
G\<turnstile>pTsa[\<preceq>]pTs; (x2, s2)\<Colon>\<preceq>(G, L);
cmethd G (target (invmode m e) s2 a' cT) (mn, pTs) =
Some (md, (ma, pns', rT'), lvars, blk, res);
G|-target (invmode m e) s2 a' cT<=:C md;
G,s2\<turnstile>a'\<Colon>\<preceq>RefT t;
invmode m e = IntVir --> a' ~= Null;
invmode m e ~= IntVir -->
(EX C. t = ClassT C & G|-C<=:C md) & cT = ClassT md |]
==> init_lvars G (target (invmode m e) s2 a' cT) (mn, pTs) (invmode m e) a' pvs
(x2, s2)\<Colon>\<preceq>(G, table_of lvars(pns'[|->]pTs) (+)
(if m then empty else empty(()|->Class md)))
theorem Call_type_sound:
[| wf_prog G; G|-(x1, s1) -ps#>pvs-> (x2, s2);
C = target (invmode m e) s2 a' cT;
s2' = init_lvars G C (mn, pTs) (invmode m e) a' pvs (x2, s2);
G|-s2' -Methd C (mn, pTs)->v-> (x3, s3);
ALL L. s2'\<Colon>\<preceq>(G, L) -->
(ALL T. (G, L)|-Methd C (mn, pTs):-T -->
(x3, s3)\<Colon>\<preceq>(G, L) &
(x3 = None --> G,s3\<turnstile>v\<Colon>\<preceq>T));
Norm s0\<Colon>\<preceq>(G, L); (G, L)|-e:-RefT t; (G, L)|-ps:#pTsa;
max_spec G t (mn, pTsa) = {((cT, m, pns, rT), pTs)};
(x1, s1)\<Colon>\<preceq>(G, L);
x1 = None --> G,s1\<turnstile>a'\<Colon>\<preceq>RefT t;
(x2, s2)\<Colon>\<preceq>(G, L);
x2 = None --> list_all2 (conf G s2) pvs pTsa |]
==> (x3, set_locals (locals s2) s3)\<Colon>\<preceq>(G, L) &
(x3 = None --> G,s3\<turnstile>v\<Colon>\<preceq>rT)
[!]
theorem eval_type_sound:
[| wf_prog G; G|-s0 -t>-> (v, s1); s0\<Colon>\<preceq>(G, L); (G, L)|-t::T |]
==> s1\<Colon>\<preceq>(G, L) &
(let (x, s) = s1
in x = None --> G,L,s\<turnstile>t\<succ>v\<Colon>\<preceq>T)
[!]
theorem eval_ts:
[| G|-s -e->v-> (x', s'); wf_prog G; s\<Colon>\<preceq>(G, L); (G, L)|-e:-T |]
==> (x', s')\<Colon>\<preceq>(G, L) &
(x' = None --> G,s'\<turnstile>v\<Colon>\<preceq>T)
[!]
theorem evals_ts:
[| G|-s -es#>vs-> (x', s'); wf_prog G; s\<Colon>\<preceq>(G, L);
(G, L)|-es:#Ts |]
==> (x', s')\<Colon>\<preceq>(G, L) &
(x' = None --> list_all2 (conf G s') vs Ts)
[!]
theorem evar_ts:
[| G|-s -v=>vf-> (x', s'); wf_prog G; s\<Colon>\<preceq>(G, L); (G, L)|-v:=T |]
==> (x', s')\<Colon>\<preceq>(G, L) &
(x' = None --> G,L,s'\<turnstile>In2 v\<succ>In2 vf\<Colon>\<preceq>Inl T)
[!]
theorem exec_ts:
[| G|-s -s0-> s'; wf_prog G; s\<Colon>\<preceq>(G, L); (G, L)|-s0:<> |]
==> s'\<Colon>\<preceq>(G, L)
[!]
theorem dyn_methods_understood:
[| wf_prog G; (G, L)|-{t,md,IntVir}e..mn( {pTs'}ps):-rT;
s\<Colon>\<preceq>(G, L); G|-s -e->a'-> Norm s'; a' ~= Null |]
==> EX a obj.
a' = Addr a &
heap s' a = Some obj & cmethd G (obj_class obj) (mn, pTs') ~= None
[!]