TypeRel.thy
Back to the index of Bali_ASCII2
(* Title: isabelle/Bali/TypeRel.thy
ID: $Id: TypeRel.thy,v 1.9 1998/04/08 15:27:11 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
The relations between Java types
*)
TypeRel = Decl +
consts
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" ("_|-_~=>1_" [71,71,71] 70)
implmt :: "prog => [tname, tname] => bool" ("_|-_~=>_" [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 ~=>1 I" == "(C,I) : implmt1 G"
"G|-C ~=> 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 &
I:set (fst (snd (the (class G C))))}"
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~=>1J ==> G|-C~=>J"
subint "[|G|-C~=>1I; G|-I<:I J|] ==> G|-C~=>J"
subcls1 "[|G|-C<:C1D; G|-D~=>J |] ==> G|-C~=>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 ==> G|- Class C<=:Iface I"
null "is_type G (RefT R) ==> G|- NT<=: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 ==>
imethds G I hidings imethds G J
entails (%(md,(pn,rT)) (md',(pn',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