TypeRel.thy
Back to the index of Bali_ASCII
(* Title: isabelle/Bali/TypeRel.thy
ID: $Id: TypeRel.thy,v 1.1 1997/10/15 19:07:12 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
The relations between Java types
*)
TypeRel = Prog +
consts (* the type variable prog stands for some program *)
subint1, (* direct subinterface *)
subint :: "prog => (tname * tname) set" (* subinterface *)
subcls1, (* direct subclass *)
subcls :: "prog => (tname * tname) set" (* subclass *)
implmt1, (* direct implementation *)
implmt :: "prog => (tname * tname) set" (* implementation *)
widen, (* widening *)
cast :: "prog => (ty * ty) set" (* casting *)
syntax (symbols)
subint1 :: "prog => [tname, tname] => bool" ("_|-_<I1_" [71,71,71] 70)
subint :: "prog => [tname, tname] => bool" ("_|-_<I _" [71,71,71] 70)
subcls1 :: "prog => [tname, tname] => bool" ("_|-_<C1_" [71,71,71] 70)
subcls :: "prog => [tname, tname] => bool" ("_|-_<C _" [71,71,71] 70)
implmt1 :: "prog => [tname, tname] => bool" ("_|-_~I1 _" [71,71,71] 70)
implmt :: "prog => [tname, tname] => bool" ("_|-_~I _" [71,71,71] 70)
widen :: "prog => [ty, ty] => bool" ("_|-_<=:_" [71,71,71] 70)
cast :: "prog => [ty, ty] => bool" ("_|-_<=:? _" [71,71,71] 70)
translations
"G|-I <I1 J" == "(I,J) : subint1 G"
"G|-I <I J" == "(I,J) : subint G"
"G|-C <C1 D" == "(C,D) : subcls1 G"
"G|-C <C D" == "(C,D) : subcls G"
"G|-C ~I1 I" == "(C,I) : implmt1 G"
"G|-C ~I I" == "(C,I) : implmt G"
"G|-S <=: T" == "(S,T) : widen G"
"G|-S <=:? T" == "(S,T) : cast G"
defs
(* direct subinterface, cf. 9.1.3 *)
subint1_def "subint1 G == {(I,J). is_iface G I & is_iface G J &
J:set (fst (the (iface G I)))}"
(* direct subclass, cf. 8.1.3 *)
subcls1_def "subcls1 G == {(C,D). is_class G C & is_class G D &
Some D = fst (the (class G C))}"
(* direct implementation, cf. 8.1.3 *)
implmt1_def "implmt1 G == {(C,I). is_class G C & is_iface G I &
Some I = fst (snd (the (class G C)))}"
consts
imethd :: "prog * tname => ( sig , ref_ty * mhead) table"
cmethd :: "prog * tname => ( sig , ref_ty * methd) table"
cfield :: "prog * tname => ( ename , ref_ty * field) table"
fields :: "prog * tname => ((ename * ref_ty) * field) list"
constdefs (* auxiliary relations for recursive definitions below *)
subint1_rel :: "((prog * tname) * (prog * tname)) set"
"subint1_rel == {((G,I),(G',I')). G = G' & wf ((subint1 G)^-1) & G|-I'<I1I}"
subcls1_rel :: "((prog * tname) * (prog * tname)) set"
"subcls1_rel == {((G,C),(G',C')). G = G' & wf ((subcls1 G)^-1) & G|-C'<C1C}"
(* methods of an interface, with overriding and inheritance, cf. 9.2 *)
recdef imethd "subint1_rel" congs "[image_cong]"
"imethd (G,I) = (if wf((subint1 G)^-1) then (case iface G I of None => arbitrary
| Some (is,ms) => (s2o o Un_tables ((%J. if is_iface G J then
imethd (G,J) else arbitrary)``set is))++
table (map (%(s,mh). (s,IfaceT I,mh)) ms))
else arbitrary)"
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
recdef cmethd "subcls1_rel"
"cmethd (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
| Some (sc,si,fs,ms) => (case sc of None => etable | Some D =>
if is_class G D then cmethd (G,D)
else arbitrary) ++
table (map (%(s, m ).
(s,(ClassT C,m))) ms))
else arbitrary)"
(* list of fields of a class, including inherited and hidden ones *)
recdef fields "subcls1_rel"
"fields (G,C) = (if wf((subcls1 G)^-1) then (case class G C of None => arbitrary
| Some (sc,si,fs,ms) => map (%(fn,ft). ((fn,ClassT C),ft)) fs@
(case sc of None => [] | Some D =>
if is_class G D then fields (G,D)
else arbitrary))
else arbitrary)"
defs
cfield_def "cfield == table o (map (%((fn,fd),ft). (fn,(fd,ft)))) o fields"
inductive "subint G" intrs (* subinterface relation, cf. 9.1.3 *)
direct "G|-I<I1K ==> G|-I<I K"
trans "[|G|-I<I J; G|-J<I K|] ==> G|-I<I K"
inductive "subcls G" intrs (* subclass relation, cf. 8.1.3 *)
direct "G|-C<C1E ==> G|-C<C E"
trans "[|G|-C<C D; G|-D<C E|] ==> G|-C<C E"
inductive "implmt G" intrs (* cf. 8.1.4 *)
direct "G|-C~I1 J ==> G|-C~I J"
subint "[|G|-C~I1 I; G|-I<I J|] ==> G|-C~I J"
subcls1 "[|G|-C<C1D; G|-D~I J |] ==> G|-C~I J"
inductive "widen G" intrs (*widening, viz. method invocation conversion, cf. 5.3
i.e. sort of syntactic subtyping *)
refl "is_type G T ==> G|- T<=:T" (* identity conv., cf. 5.1.1 *)
subint "G|-I<I J ==> G|- Iface I<=:Iface J"(*wid. ref.conv,cf. 5.1.4 *)
int_obj"is_iface G I ==>
is_class G Object ==> G|- Iface I<=:Class Object"
subcls "G|-C<C D ==> G|- Class C<=:Class D"
implmt "G|-C~I I ==> G|- Class C<=:Iface I"
null "is_type G (RefT R) ==> G|-RefT NullT<=:RefT R"
arr_obj"is_type G T ==>
is_class G Object ==> G|- T[.]<=:Class Object"
array "G|-RefT S<=:RefT T ==> G|-RefT S[.]<=:RefT T[.]"
inductive "cast G" intrs (* casting / narr.ref. conversion, cf. 5.5 / 5.1.5 *)
widen "G|-S<=:T ==> G|- S<=:? T"
subcls "G|-C<C D ==> G|- Class D<=:? Class C"
implmt "is_class G C ==>
is_iface G I ==> G|- Class C<=:? Iface I"
obj_arr"is_class G Object ==>
is_type G T ==> G|-Class Object<=:? T[.]"
int_cls"is_iface G I ==>
is_class G C ==> G|- Iface I<=:? Class C"
subint "is_iface G I ==>
is_iface G J ==>
imethd (G,I) hiding imethd (G,J)
entails (%(md,rT) (md',rT'). G|-rT<=:rT') ==>
~ G|-I<I J ==> G|- Iface I<=:? Iface J"
array "G|-RefT S<=:? RefT T ==> G|- RefT S[.]<=:? RefT T[.]"
end