Up to index of Isabelle/Bali5
theory WellType = TypeRel(* Title: isabelle/Bali/WellType.thy
ID: $Id: WellType.thy,v 1.43 2000/11/28 23:06:20 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Well-typedness of Java programs
improvements over Java Specification 1.0:
* methods of Object can be called upon references of interface or array type
simplifications:
* the type rules include all static checks on statements and expressions, e.g.
definedness of names (of parameters, locals, fields, methods)
design issues:
* unified type judgment for statements, variables, expressions, expression lists
* statements are typed like expressions with dummy type Void
* the typing rules take an extra argument that is capable of determining
the dynamic type of objects. Therefore, they can be used for both
checking static types and determining runtime types in transition semantics.
*)
WellType = TypeRel +
types lenv
= "(lname, ty) table" (* local variables, including This *)
env
= "prog × lenv" (* program, locals *)
syntax
prg :: "env \<Rightarrow> prog"
lcl :: "env \<Rightarrow> lenv"
translations
"lenv" <= (type) "(lname, ty) table"
"env" <= (type) "prog × lenv"
"prg" => "fst"
"lcl" => "snd"
types
emhead = "ref_ty × mhead"
consts
cmheads :: "prog \<Rightarrow> tname \<Rightarrow> sig \<Rightarrow> emhead set"
mheads :: "prog \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
defs
cmheads_def
"cmheads G C \<equiv> \<lambda>sig. (\<lambda>(C,(h,b)). (ClassT C,h)) `` o2s (cmethd G C sig)"
primrec
"mheads G NullT = (\<lambda>sig. {})"
"mheads G (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) `` imethds G I sig \<union>
cmheads G Object sig)"
"mheads G (ClassT C) = cmheads G C"
"mheads G (ArrayT T) = cmheads G Object"
(* more detailed than necessary for type-safety, see below. *)
constdefs
(* applicable methods, cf. 15.11.2.1 *)
appl_methds :: "prog \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead × ty list) set"
"appl_methds G rt \<equiv> \<lambda>(mn, pTs). {(mh,pTs') |mh pTs'.
mh \<in> mheads G rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'}"
(* more specific methods, cf. 15.11.2.2 *)
more_spec :: "prog \<Rightarrow> emhead × ty list \<Rightarrow> emhead × ty list \<Rightarrow> bool"
"more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
(* maximally specific methods, cf. 15.11.2.2 *)
max_spec :: "prog \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead × ty list) set"
" max_spec G rt sig \<equiv>{m. m \<in>appl_methds G rt sig \<and>
(\<forall>m'\<in>appl_methds G rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
(*
rules (* all properties of more_spec, appl_methods and max_spec we actually need
these can easily be proven from the above definitions *)
max_spec2mheads "max_spec G rt (mn, pTs) = insert (mh, pTs') A \<Longrightarrow>
mh\<in>mheads G rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'"
*)
constdefs
empty_dt :: "dyn_ty"
"empty_dt \<equiv> \<lambda>a. None"
invmode :: "modi \<Rightarrow> expr \<Rightarrow> inv_mode"
"invmode m e \<equiv> if static m then Static else if e=Super then SuperM else IntVir"
types tys = "ty + ty list"
translations
"tys" <= (type) "ty + ty list"
consts
wt :: "(env × dyn_ty × term × tys) set"
(*wt :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term × tys) set" not feasible because of
changing env in Try stmt *)
syntax
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51 ] 50)
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
ty list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
syntax (xsymbols)
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50)
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50)
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
ty list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
translations
"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
"E,dt\<Turnstile>s\<Colon>\<surd>" == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2 e\<Colon>Inl T"
"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3 e\<Colon>Inr T"
syntax (* for purely static typing *)
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
ty_exprs_:: "env \<Rightarrow> [expr list,
ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
syntax (xsymbols)
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50)
wt_stmt_:: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50)
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
ty_exprs_:: "env \<Rightarrow> [expr list,
ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
translations
"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>"
"E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T"
"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T"
"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
inductive wt intrs
(* well-typed statements *)
Skip "E,dt\<Turnstile>Skip\<Colon>\<surd>"
Expr "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Expr e\<Colon>\<surd>"
Comp "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>;
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
(* cf. 14.8 *)
If "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
E,dt\<Turnstile>c1\<Colon>\<surd>;
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
(* cf. 14.10 *)
Loop "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>While(e) c\<Colon>\<surd>"
(* cf. 14.16 *)
Throw "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
prg E\<turnstile>tn\<preceq>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Throw e\<Colon>\<surd>"
(* cf. 14.18 *)
Try "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>C SXcpt Throwable;
lcl E (EName vn)=None; (prg E,lcl E(EName vn\<mapsto>Class tn)),dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
(* cf. 14.18 *)
Fin "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
Init "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>init C\<Colon>\<surd>"
(* well-typed expressions *)
(* cf. 15.8 *)
NewC "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>NewC C\<Colon>-Class C"
(* cf. 15.9 *)
NewA "\<lbrakk>is_type (prg E) T;
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
(* cf. 15.15 *)
Cast "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_type (prg E) T';
prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Cast T' e\<Colon>-T'"
(* cf. 15.19.2 *)
Inst "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T;
prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
(* cf. 15.7.1 *)
Lit "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Lit x\<Colon>-T"
(* cf. 15.10.2, 15.11.1 *)
Super "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
class (prg E) C = Some (D, rest)\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Super\<Colon>-Class D"
(* cf. 15.13.1, 15.10.1, 15.12 *)
Acc "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Acc va\<Colon>-T"
(* cf. 15.25, 15.25.1 *)
Ass "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
E,dt\<Turnstile>v \<Colon>-T';
prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>va:=v\<Colon>-T'"
(* cf. 15.24 *)
Cond "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
(* cf. 15.11.1, 15.11.2, 15.11.3 *)
Call "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT t;
E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
max_spec (prg E) t (mn, pTs) = {((md,(m,pns,rT)),pTs')}\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>{t,md,invmode m e}e..mn({pTs'}ps)\<Colon>-rT"
Methd "\<lbrakk>is_class (prg E) C;
cmethd (prg E) C sig = Some (md,mh,lvars,blk,res);
E,dt\<Turnstile>Body md blk res\<Colon>-T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Methd C sig\<Colon>-T"
Body "\<lbrakk>is_class (prg E) D;
E,dt\<Turnstile>blk\<Colon>\<surd>;
E,dt\<Turnstile>res\<Colon>-T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>Body D blk res\<Colon>-T"
(* well-typed variables *)
(* cf. 15.13.1 *)
LVar "\<lbrakk>lcl E vn = Some T; is_type (prg E) T\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>LVar vn\<Colon>=T"
(* cf. 15.10.1 *)
FVar "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C;
cfield (prg E) C fn = Some (fd,(m,fT))\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>{fd,static m}e..fn\<Colon>=fT"
(* cf. 15.12 *)
AVar "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[];
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>e.[i]\<Colon>=T"
(* well-typed expression lists *)
(* cf. 15.11.??? *)
Nil "E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
(* cf. 15.11.??? *)
Cons "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
end
theorem invmode_nonstatic:
invmode False (Acc (LVar e)) = IntVir [!]
theorem invmode_Static_eq:
(invmode m e = Static) = m
theorem invmode_IntVir_eq:
(invmode m e = IntVir) = (¬ m & e ~= Super)
theorem Null_staticD:
a' = Null --> m ==> invmode m e = IntVir --> a' ~= Null
theorem wt_Methd_is_methd:
(G, L)|-In1l (Methd C sig)::T ==> is_methd G C sig [!]
theorem wt_Call:
[| E,dt|=e:-RefT t; E,dt|=ps:#pTs;
max_spec (fst E) t (mn, pTs) = {((md, m, pns, rT), pTs')};
mode = invmode m e |]
==> E,dt|={t,md,mode}e..mn( {pTs'}ps):-rT
theorem wt_init:
(E,dt|=init C:<>) = is_class (fst E) C [!]
theorem wt_StatRef:
isrtype (fst E) rt ==> E|-StatRef rt:-RefT rt
theorem wt_Inj_elim:
E,dt|=t::U
==> sum3_case ((%e. EX T. U = Inl T) (+) (%s. U = Inl (PrimT Void)))
(%e. EX T. U = Inl T) (%e. EX T. U = Inr T) t
theorem wt_expr_eq:
(E,dt|=In1l t::U) = (EX T. U = Inl T & E,dt|=t:-T)
theorem wt_var_eq:
(E,dt|=In2 t::U) = (EX T. U = Inl T & E,dt|=t:=T)
theorem wt_exprs_eq:
(E,dt|=In3 t::U) = (EX Ts. U = Inr Ts & E,dt|=t:#Ts)
theorem wt_stmt_eq:
(E,dt|=In1r t::U) = (U = Inl (PrimT Void) & E,dt|=t:<>)
theorem Inj_eq_lemma:
(ALL T. (EX T'. T = Inj T' & P T') --> Q T) = (ALL T'. P T' --> Q (Inj T'))
theorem univalent_tys_lemma:
[| ALL S T. G|-S<=:T --> G|-T<=:S --> S = T; E,dt|=t::T; G = fst E;
E,dt|=t::T' |]
==> T = T'
[!]
theorem univalent_tys:
ws_prog (fst E) ==> univalent {(t, T). E,dt|=t::T} [!]
theorem typeof_empty_is_type:
typeof (%a. None) v = Some T ==> is_type G T
theorem typeof_is_type:
ALL a. v ~= Addr a ==> EX T. typeof dt v = Some T & is_type G T
theorem max_spec2appl_meths:
x : max_spec G T sig ==> x : appl_methds G T sig
theorem appl_methsD:
(mh, pTs') : appl_methds G T (mn, pTs) ==> mh : mheads G T (mn, pTs') & G\<turnstile>pTs[\<preceq>]pTs'
theorem max_spec2mheads:
max_spec G T (mn, pTs) = insert (mh, pTs') B ==> mh : mheads G T (mn, pTs') & G\<turnstile>pTs[\<preceq>]pTs'