Decl.thy
Back to the index of Bali_ASCII2
(* Title: isabelle/Bali/Decl.thy
ID: $Id: Decl.thy,v 1.7 1998/04/08 15:26:55 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Field, method, interface, and class declarations, whole Java programs
simplifications:
* no field modifiers yet, i.e. every field is public, non-static, non-final
* no method modifiers yet, i.e. every method is public, non-static, non-final
* no throws clause
* result statement replaced by result expression (evaluated at the end of the
execution of the body; transformation is always possible (with goto, while)
* a void method is replaced by one that returns Unit of dummy type Void
* local variables are initialzed with default values
* each method has exactly one (explicit) parameter; this may be an object with
as many fields as required if the method has more than one parameter
* no interface modifiers yet, i.e. every interface is public
* no interface fields yet
* no class modifiers yet, i.e. every class is public, non-final
* every class except Object has an explicit superclass
* Object does not have any standard methods
* no packages
* no main method yet
*)
Decl = Term +
types field
= "ty"
fdecl (* field declaration, cf. 8.3 (, 9.3) *)
= "ename * field"
types sig (* signature of a method, cf. 8.4.2 *)
= "mname * ty" (* method name, parameter type *)
mhead (* method head (excluding signature) *)
= "ename * ty" (* parameter name, result type *)
lvar (* local variable *)
= "ename * ty"
mbody (* method body *)
= "lvar list * stmt * expr"
(* local variables, block, result expression *)
methd (* method in a class *)
= "mhead * mbody"
mdecl (* method declaration in a class *)
= "sig * methd"
types iface (* interface *)
= "tname list * (sig * mhead) list"
(* superinterface list, methods *)
idecl (* interface declaration, cf. 9.1 *)
= "tname * iface"
types class (* class *)
= "tname option * tname list * fdecl list * mdecl list"
(* superclass, implemented interfaces, fields, methods*)
cdecl (* class declaration, cf. 8.1 *)
= "tname * class"
consts
ObjectC :: "cdecl" (* declaration of root class *)
SXcptC :: "xname => cdecl" (* declarations of throwable classes *)
defs
ObjectC_def "ObjectC == (Object , (None , [], [], []))"
SXcptC_def "SXcptC xn== (SXcpt xn, (Some (if xn = Throwable then Object else
SXcpt Throwable), [], [], []))"
types prog = "idecl list * cdecl list"
syntax
iface :: "prog => (tname, iface) table"
class :: "prog => (tname, class) table"
translations
"iface G" == "table_of (fst G)"
"class G" == "table_of (snd G)"
consts
is_iface :: "prog => tname => bool"
is_class :: "prog => tname => bool"
is_type :: "prog => ty => bool"
isrtype :: "prog => ref_ty => bool"
defs
is_iface_def "is_iface G I == iface G I ~= None"
is_class_def "is_class G C == class G C ~= None"
primrec is_type ty
"is_type G (PrimT pt) = True"
"is_type G (RefT rt) = isrtype G rt"
primrec isrtype Rt (** ref_ty **)
"isrtype G (NullT ) = True"
"isrtype G (IfaceT tn) = is_iface G tn"
"isrtype G (ClassT tn) = is_class G tn"
"isrtype G (ArrayT T ) = is_type G T"
consts
(* general operators for recursion over the interace and class hiearchies *)
iface_rec :: " tname * prog * (tname => iface => 'a set => 'a) => 'a"
class_rec :: " tname * prog * 'a * (tname => class => 'a => 'a) => 'a"
(* auxiliary relations for recursive definitions below *)
iface_wfrel :: "((tname * prog * (tname => iface => 'a set => 'a)) *
(tname * prog * (tname => iface => 'a set => 'a))) set"
class_wfrel :: "((tname * prog * 'a * (tname => class => 'a => 'a)) *
(tname * prog * 'a * (tname => class => 'a => 'a))) set"
recdef iface_rec "iface_wfrel" congs "[image_cong]"
"iface_rec (I,G, f) = (if (!i J. iface G I = Some i & J : set (fst i) -->
((J,G, f), (I,G, f)) : iface_wfrel)
then (case iface G I of None => arbitrary | Some i =>
f I i ((%J. iface_rec (J,G, f))``set (fst i)))
else arbitrary)"
recdef class_rec "class_wfrel"
"class_rec (C,G,t,f) = (if (!c D. class G C = Some c & Some D = (fst c) -->
((D,G,t,f), (C,G,t,f)) : class_wfrel)
then (case class G C of None => arbitrary | Some c =>
f C c (case (fst c) of None => t | Some D =>
class_rec (D,G,t,f)))
else arbitrary)"
consts
imethds :: "prog => tname => ( sig , ref_ty * mhead) tables"
cmethd :: "prog => tname => ( sig , ref_ty * methd) table"
cfield :: "prog => tname => ( ename , ref_ty * field) table"
fields :: "prog => tname => ((ename * ref_ty) * field) list"
defs
(* methods of an interface, with overriding and inheritance, cf. 9.2 *)
imeths_def "imethds G I == iface_rec (I,G, (%I (is,ms) ts.
(Un_tables ts) ++++ (o2s o table_of (map (%(s,mh). (s,IfaceT I,mh)) ms))))"
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
cmethd_def "cmethd G C == class_rec (C,G,empty,(%C (sc,si,fs,ms) ts.
ts ++ table_of (map (%(s,m ). (s,(ClassT C,m))) ms)))"
(* list of fields implemented by a class, including inherited and hidden ones *)
fields_def "fields G C == class_rec (C,G,[] ,(%C (sc,si,fs,ms) ts.
map (%(fn,ft).((fn,ClassT C),ft)) fs @ ts))"
(* fields of a class, with inheritance and hiding, cf. 8.3 *)
cfield_def "cfield G C == table_of((map (%((n,d),t).(n,(d,t)))) (fields G C))"
end