WellType.thy
Back to the index of Bali_ASCII2
(* Title: isabelle/Bali/WellType.thy
ID: $Id: WellType.thy,v 1.7 1998/04/08 15:27:14 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Well-typedness of Java programs
the formulation of well-typedness of method calls given below (as well as
the Java Specification 1.0) is a little too restrictive: Is does not allow
methods of class Object to be called upon references of interface type.
simplifications:
* the type rules include all static checks on expressions and statements, e.g.
definedness of names (of parameters, locals, fields, methods)
design issues:
* 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
= "(ename, ty) table" (* local variables, including This *)
env
= "prog * lenv" (* program, locals *)
dyn_ty
= "loc => ty option"
syntax
prg :: "env => prog"
lcl :: "env => lenv"
translations
"prg" => "fst"
"lcl" => "snd"
consts
more_spec :: "prog => (ref_ty * mhead) * ty => (ref_ty * mhead) * ty => bool"
mheads :: "prog => ref_ty => sig => (ref_ty * mhead) set"
appl_methds :: "prog => ref_ty => sig =>((ref_ty * mhead) * ty) set"
max_spec :: "prog => ref_ty => sig =>((ref_ty * mhead) * ty) set"
primrec mheads Rt (** ref_ty **)
"mheads G NullT = (%sig. {})"
"mheads G (IfaceT I) = imethds G I"
"mheads G (ClassT C) = o2s o option_map (%(md,(mh,mb)).(md,mh)) o cmethd G C"
"mheads G (ArrayT T) = (%sig. {})"
defs
more_spec_def "more_spec G == %((md,mh),pT). %((md',mh'),pT').
G|-RefT md<=:RefT md'& G|-pT<=:pT'"
(* applicable methods, cf. 15.11.2.1 *)
appl_methds_def "appl_methds G T == %(mn, pT). {(mh,pT') |mh pT'.
mh : mheads G T (mn, pT') & G|-pT<=:pT'}"
(* maximally specific methods, cf. 15.11.2.2 *)
max_spec_def "max_spec G T sig == {m. m :appl_methds G T sig &
(!m':appl_methds G T sig.
more_spec G m' m --> m' = m)}"
consts
typeof :: "dyn_ty => val => ty option"
primrec typeof val_ (** val **)
"typeof dt Unit = Some (PrimT Void)"
"typeof dt (Bool b) = Some (PrimT Boolean)"
"typeof dt (Intg i) = Some (PrimT IntDefer)"
"typeof dt Null = Some NT"
"typeof dt (Addr a) = dt a"
consts
ty_exprs :: " env => dyn_ty => (expr * ty) set"
wt_stmts :: "(env * dyn_ty * stmt ) set"
(*wt_stmts :: " env => dyn_ty => stmt set" not feasible because of
changing env in Try stmt *)
syntax
ty_expr :: "env => dyn_ty => [expr,ty] => bool" ("_,_|=_::_" [51,51,51,51] 50)
wt_stmt :: "env => dyn_ty => stmt => bool" ("_,_|=_::<>" [51,51,51 ] 50)
translations
"E,dt|=ex::T" == "(ex,T) : ty_exprs E dt"
"E,dt|=s ::<>" == "(E,dt,s) : wt_stmts"
syntax
ty_expr_ :: "env => [expr, ty] => bool" ("_|-_::_" [51,51,51] 50)
wt_stmt_ :: "env => stmt => bool" ("_|-_::<>" [51,51 ] 50)
constdefs empty_dt :: dyn_ty "empty_dt == %a. None" (* for static typing *)
translations
"E|-ex::T" == "E,empty_dt|=ex::T"
"E|-s ::<>" == "E,empty_dt|=s ::<>"
inductive "ty_exprs E dt" intrs (* well-typed expressions *)
(* cf. 15.8 *)
NewC "[|is_class (prg E) C|] ==>
E,dt|=NewC C::Class C"
(* cf. 15.9 *)
NewA "[|is_type (prg E) T;
E,dt|=i::PrimT IntDefer|] ==>
E,dt|=New T[i]::T[.]"
(* cf. 15.15 *)
Cast "[|E,dt|=e::T;
prg E|-T<=:? T'|] ==>
E,dt|=Cast T' e::T'"
(* cf. 15.7.1 *)
Lit "[|typeof dt x = Some T|] ==>
E,dt|=Lit x::T"
(* cf. 15.13.1 *)
LAcc "[|lcl E vn = Some T; is_type (prg E) T|] ==>
E,dt|=LAcc vn::T"
(* cf. 15.25, 15.25.1 *)
LAss "[|E,dt|=LAcc vn::T; vn ~= This;
E,dt|=v ::T';
prg E|-T'<=:T|] ==>
E,dt|=vn:=v::T'"
(* cf. 15.10.1 *)
FAcc "[|E,dt|=a::Class C;
cfield (prg E) C fn = Some (fd,fT)|] ==>
E,dt|=a.{fd}fn::fT"
(* cf. 15.25, 15.25.1 *)
FAss "[|E,dt|=a.{fd}fn::T;
E,dt|=v ::T';
prg E|-T'<=:T|] ==>
E,dt|=a.{fd}fn:=v::T'"
(* cf. 15.12 *)
AAcc "[|E,dt|=a::T[.];
E,dt|=i::PrimT IntDefer|] ==>
E,dt|=a[i]::T"
(* cf. 15.25, 15.25.1 *)
AAss "[|E,dt|=a[i]::T;
E,dt|=v ::T';
prg E|-T'<=:T|] ==>
E,dt|=a[i]:=v::T'"
(* cf. 15.11.1, 15.11.2, 15.11.3 *)
Call "[|E,dt|=a::RefT T;
E,dt|=p::pT;
max_spec (prg E) T (mn, pT) = {((md,(pn,rT)),pT')}|] ==>
E,dt|=a..mn{pT'}(p)::rT"
inductive wt_stmts intrs (* well-typed statements *)
Skip "E,dt|=Skip::<>"
Expr "[|E,dt|=e::T|] ==>
E,dt|=Expr e::<>"
Comp "[|E,dt|=c1::<>;
E,dt|=c2::<>|] ==>
E,dt|=c1;; c2::<>"
(* cf. 14.8 *)
Cond "[|E,dt|=e::PrimT Boolean;
E,dt|=c1::<>;
E,dt|=c2::<>|] ==>
E,dt|=If(e) c1 Else c2::<>"
(* cf. 14.10 *)
Loop "[|E,dt|=e::PrimT Boolean;
E,dt|=c::<>|] ==>
E,dt|=While(e) c::<>"
(* cf. 14.16 *)
Throw "[|E,dt|=e::Class tn;
prg E|-Class tn<=:Class (SXcpt Throwable)|] ==>
E,dt|=Throw e::<>"
(* cf. 14.18 *)
Try "[|E,dt|=c1::<>; prg E|-Class tn<=:Class (SXcpt Throwable);
lcl E vn = None; (prg E,lcl E[vn|->Class tn]),dt|=c2::<>|] ==>
E,dt|=Try c1 Catch(tn vn) c2::<>"
(* cf. 14.18 *)
Fin "[|E,dt|=c1::<>; E,dt|=c2::<>|] ==>
E,dt|=c1 Finally c2::<>"
end