WellType.thy
Back to the index of Bali_ASCII
(* Title: isabelle/Bali/WellType.thy
ID: $Id: WellType.thy,v 1.2 1997/10/22 12:00:15 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 concerns:
* 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 env
= "prog * ty * tname"
(* program, method parameter, current class *)
dyn_ty
= "loc => ty option"
syntax
prg :: "env => prog"
localT :: "env => (ename, ty) table"
thisT :: "env => tname"
translations
"prg" => "first"
"localT" => "secnd"
"thisT" => "third"
consts
more_spec :: "prog => (ref_ty * mhead) * ty => (ref_ty * mhead) * ty => bool"
m_head :: "prog => ref_ty => sig => (ref_ty * mhead) option"
appl_methds :: "prog => ref_ty => sig =>((ref_ty * mhead) * ty) set"
max_spec :: "prog => ref_ty => sig =>((ref_ty * mhead) * ty) set"
defs
m_head_def "m_head G t sig == case t of NullT => None
| IfaceT I => imethd (G,I) sig
| ClassT C => option_map (%(md,(mh,mb)). (md,mh))
(cmethd (G,C) sig)
| ArrayT T => None"
more_spec_def "more_spec G==%((d,r),p).%((d',r'),p').G|-RefT d<=:RefT d'& G|-p<=:p'"
(* applicable methods, cf. 15.11.2.1 *)
appl_methds_def "appl_methds G rT == %(mn, pT). {(mh,pT') |mh pT'.
m_head G rT (mn, pT') = Some mh & G|-pT<=:pT'}"
(* maximally specific methods, cf. 15.11.2.2 *)
max_spec_def "max_spec G rT sig == {m. m :appl_methds G rT sig &
(!m':appl_methds G rT sig.
more_spec G m' m --> m' = m)}"
consts
typeof:: "dyn_ty => val => ty option"
primrec typeof val_
"typeof dt Unit = Some (PrimT Void)"
"typeof dt Null = Some (RefT NullT)"
"typeof dt (Bool b) = Some (PrimT Boolean)"
"typeof dt (Intg i) = Some (PrimT IntDefer)"
"typeof dt (Addr a) = dt a"
consts
ty_exprs :: "env => dyn_ty => (expr * ty) set"
wt_stmts :: "env => dyn_ty => stmt set"
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 ::<>" == " s : wt_stmts E dt"
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"
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.7.2 *)
This "[|is_class (prg E) (thisT E)|] ==>
E,dt|=This::Class (thisT E)"
(* 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|=NewA 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 "[|is_type (prg E) (localT E)|] ==>
E,dt|=LAcc::localT E"
(* cf. 15.25, 15.25.1 *)
LAss "[|E,dt|=v::T;
prg E|-T<=:localT E|] ==>
E,dt|=LAss 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,rT),pT')}|] ==>
E,dt|=a..mn{pT'}(p)::rT"
inductive "wt_stmts E dt" intrs (* well-typed statements *)
Skip "E,dt|=Skip::<>"
Expr "[|E,dt|=e::T|] ==>
E,dt|=Expr e::<>"
Comp "[|E,dt|=s1::<>;
E,dt|=s2::<>|] ==>
E,dt|=s1;; s2::<>"
(* cf. 14.8 *)
Cond "[|E,dt|=e::PrimT Boolean;
E,dt|=s1::<>;
E,dt|=s2::<>|] ==>
E,dt|=If(e) s1 Else s2::<>"
(* cf. 14.10 *)
Loop "[|E,dt|=e::PrimT Boolean;
E,dt|=s::<>|] ==>
E,dt|=While(e) s::<>"
end