Up to index of Isabelle/Bali4
theory Decl = Term + Table(* Title: isabelle/Bali/Decl.thy
ID: $Id: Decl.thy,v 1.38 2000/07/25 21:54:10 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Field, method, interface, and class declarations, whole Java programs
simplifications:
* the only field and method modifier is static
* no constructors, which may be simulated by new + suitable methods
* there is just one global initializer per class, which can simulate all others
* 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)
* no interface modifiers yet, i.e. every interface is public
* no interface fields
* no class modifiers yet, i.e. every class is public, non-final
* every class has an explicit superclass (unused for Object)
* the (standard) methods of Object and of standard exceptions are not specified
* no packages
* no main method
*)
Decl = Term + Table + (** order is significant, because of clash for "var" **)
types modi = bool (* modifier: static *)
field
= "modi × ty"
fdecl (* field declaration, cf. 8.3 *)
= "ename × field"
translations
"field" <= (type) "bool × ty"
"fdecl" <= (type) "ename × field"
types (*sig: see Term.thy *)
mhead (* method head (excluding signature) *)
= "modi × ename list × ty"
(* modifier, parameter names, result type *)
mbody (* method body *)
= "(ename × ty) list × stmt × expr"
(* local variables, block+result expression *)
methd (* method in a class *)
= "mhead × mbody"
mdecl (* method declaration in a class *)
= "sig × methd"
translations
"mhead" <= (type) "bool × ename list × ty"
"mbody" <= (type) "(ename × ty) list × stmt × expr"
"methd" <= (type) "mhead × mbody"
"mdecl" <= (type) "sig × methd"
syntax
static :: "modi \<Rightarrow> bool"
mrt :: "mhead \<Rightarrow> ty"
translations
"static" => "id"
"mrt mh" => "snd (snd mh)"
types ibody (* interface body *)
= "(sig × mhead) list"
(* methods *)
iface (* interface *)
= "tname list × ibody"
(* superinterface list *)
idecl (* interface declaration, cf. 9.1 *)
= "tname × iface"
translations
"ibody" <= (type) "(sig × mhead) list"
"iface" <= (type) "tname list × ibody"
"idecl" <= (type) "tname × iface"
types cbody (* class body *)
= "fdecl list × mdecl list × stmt"
(* fields, methods, initializer *)
class (* class *)
= "tname × tname list × cbody"
(* superclass, implemented interfaces *)
cdecl (* class declaration, cf. 8.1 *)
= "tname × class"
translations
"cbody" <= (type) "fdecl list × mdecl list × stmt"
"class" <= (type) "tname × tname list × cbody"
"cdecl" <= (type) "tname × class"
consts
Object_mdecls :: "mdecl list" (* methods of Object *)
SXcpt_mdecls :: "mdecl list" (* methods of SXcpts *)
ObjectC :: "cdecl" (* declaration of root class *)
SXcptC ::"xname \<Rightarrow> cdecl" (* declarations of throwable classes *)
standard_classes :: cdecl list
defs
ObjectC_def "ObjectC \<equiv> (Object , (arbitrary ,[],[],Object_mdecls,Skip))"
SXcptC_def "SXcptC xn\<equiv> (SXcpt xn, (if xn = Throwable then Object else
SXcpt Throwable,[],[],SXcpt_mdecls,Skip))"
standard_classes_def "standard_classes \<equiv> [ObjectC, SXcptC Throwable,
SXcptC NullPointer, SXcptC OutOfMemory, SXcptC ClassCast,
SXcptC NegArrSize , SXcptC IndOutBound, SXcptC ArrStore]"
(* programs *)
types prog = "idecl list × cdecl list"
translations
"prog"<= (type) "idecl list × cdecl list"
syntax
iface :: "prog \<Rightarrow> (tname, iface) table"
class :: "prog \<Rightarrow> (tname, class) table"
is_iface :: "prog \<Rightarrow> tname \<Rightarrow> bool"
is_class :: "prog \<Rightarrow> tname \<Rightarrow> bool"
translations
"iface G I" == "table_of (fst G) I"
"class G C" == "table_of (snd G) C"
"is_iface G I" == "iface G I \<noteq> None"
"is_class G C" == "class G C \<noteq> None"
consts
is_type :: "prog \<Rightarrow> ty \<Rightarrow> bool"
isrtype :: "prog \<Rightarrow> ref_ty \<Rightarrow> bool"
primrec "is_type G (PrimT pt) = True"
"is_type G (RefT rt) = isrtype G rt"
"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"
(* subinterface and subclass relation, in anticipation of TypeRel.thy *)
consts
subint1,
subcls1 :: "prog \<Rightarrow> (tname × tname) set"
defs
subint1_def "subint1 G \<equiv> {(I,J). \<exists>i\<in>iface G I: J\<in>set (fst i)}"
subcls1_def "subcls1 G \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c\<in>class G C: fst c = D)}"
(* well-structured programs *)
constdefs
ws_idecl :: "prog \<Rightarrow> tname \<Rightarrow> tname list \<Rightarrow> bool"
"ws_idecl G I si \<equiv> \<forall>J\<in>set si. is_iface G J \<and> (J,I)\<notin>(subint1 G)^+"
ws_cdecl :: "prog \<Rightarrow> tname \<Rightarrow> tname \<Rightarrow> bool"
"ws_cdecl G C sc \<equiv> C\<noteq>Object \<longrightarrow> is_class G sc \<and> (sc,C)\<notin>(subcls1 G)^+"
ws_prog :: "prog \<Rightarrow> bool"
"ws_prog G \<equiv> (\<forall>(I,(si,ib))\<in>set (fst G). ws_idecl G I si) \<and>
(\<forall>(C,(sc,cb))\<in>set (snd G). ws_cdecl G C sc)"
(* auxiliary well-founded relation for the recursion operators below *)
constdefs
ws_wfrel :: "(prog \<Rightarrow> (tname × tname) set) \<Rightarrow>
((prog × tname) × (prog × tname)) set"
"ws_wfrel R \<equiv> {((G,I),(G',I')). G' = G \<and> ws_prog G \<and> (I',I) \<in> R G}"
(* general operators for recursion over the interface and class hiearchies *)
consts
iface_rec :: "prog × tname \<Rightarrow> \<spacespace> (tname \<Rightarrow> ibody \<Rightarrow> 'a set \<Rightarrow> 'a) \<Rightarrow> 'a"
class_rec :: "prog × tname \<Rightarrow> 'a \<Rightarrow> (tname \<Rightarrow> cbody \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a"
recdef iface_rec "ws_wfrel subint1" congs image_cong
"iface_rec (G,I) = (\<lambda>f. case iface G I of None \<Rightarrow> arbitrary | Some (si,ib) \<Rightarrow>
if ws_prog G then f I ib ((\<lambda>J. iface_rec (G,J) f)``set si)
else arbitrary)"
recdef class_rec "ws_wfrel subcls1"
"class_rec(G,C) = (\<lambda>t f. case class G C of None\<Rightarrow> arbitrary | Some (sc,si,cb)\<Rightarrow>
if ws_prog G then f C cb (if C = Object then t else class_rec (G,sc) t f)
else arbitrary)"
types
fspec = "ename × tname"
consts
imethds :: "prog \<Rightarrow> tname \<Rightarrow> ( sig , tname × mhead) tables"
cmethd :: "prog \<Rightarrow> tname \<Rightarrow> ( sig , tname × methd) table"
fields :: "prog \<Rightarrow> tname \<Rightarrow> ((ename × tname) × field) list"
cfield :: "prog \<Rightarrow> tname \<Rightarrow> ( ename , tname × field) table"
defs
(* methods of an interface, with overriding and inheritance, cf. 9.2 *)
imeths_def "imethds G I \<equiv> iface_rec (G,I) (\<lambda>I ms ts.
(Un_tables ts) \<oplus>\<oplus> (o2s \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) ms)))"
(* methods of a class, with inheritance, overriding and hiding, cf. 8.4.6 *)
cmethd_def "cmethd G C \<equiv> class_rec (G,C) empty (\<lambda>C (fs,ms,ini) ts.
\<spacespace> ts \<oplus> table_of (map (\<lambda>(s,m). (s,C,m)) ms))"
(* list of fields of a class, including inherited and hidden ones *)
fields_def "fields G C \<equiv> class_rec (G,C) [] (\<lambda>C (fs,ms,ini) ts.
\<spacespace> map (\<lambda>(n,t). ((n,C),t)) fs @ ts)"
(* fields of a class, with inheritance and hiding, cf. 8.3 *)
cfield_def "cfield G C \<equiv> table_of((map (\<lambda>((n,d),T).(n,(d,T)))) (fields G C))"
constdefs
is_methd :: "prog \<Rightarrow> tname \<Rightarrow> sig \<Rightarrow> bool"
"is_methd G \<equiv> \<lambda>C sig. is_class G C \<and> cmethd G C sig \<noteq> None"
end
theorem ObjectC_neq_SXcptC:
ObjectC ~= SXcptC xn
theorem SXcptC_inject:
(SXcptC xn = SXcptC xm) = (xn = xm)
theorem type_is_iface:
is_type G (Iface I) ==> is_iface G I
theorem type_is_class:
is_type G (Class C) ==> is_class G C
theorem ws_progI:
[| ALL (I, si, ib):set (fst G).
ALL J:set si. is_iface G J & (J, I) ~: (subint1 G)^+;
ALL (C, D, cb):set (snd G).
C ~= Object --> is_class G D & (D, C) ~: (subcls1 G)^+ |]
==> ws_prog G
theorem ws_prog_ideclD:
[| iface G I = Some (si, ib); J : set si; ws_prog G |] ==> is_iface G J & (J, I) ~: (subint1 G)^+
theorem ws_prog_cdeclD:
[| class G C = Some (sc, cb); C ~= Object; ws_prog G |] ==> is_class G sc & (sc, C) ~: (subcls1 G)^+
theorem subint1I:
[| iface G I = Some (si, ms); J : set si |] ==> (I, J) : subint1 G
theorem subcls1I:
[| class G C = Some (D, rest); C ~= Object |] ==> (C, D) : subcls1 G
theorem subint1D:
(I, J) : subint1 G ==> ? (si, ms):iface G I: J : set si
theorem subcls1D:
(C, D) : subcls1 G ==> C ~= Object & (EX cb. class G C = Some (D, cb))
theorem subint1_def2:
subint1 G = (SIGMA I:dom (table_of (fst G)). set (fst (the (iface G I))))
theorem subcls1_def2:
subcls1 G =
(SIGMA C:dom (table_of (snd G)). {D. C ~= Object & fst (the (class G C)) = D})
theorem finite_subint1:
finite (subint1 G)
theorem finite_subcls1:
finite (subcls1 G)
theorem subint1_irrefl_lemma1:
ws_prog G ==> (subint1 G)^-1 Int (subint1 G)^+ = {}
theorem subcls1_irrefl_lemma1:
ws_prog G ==> (subcls1 G)^-1 Int (subcls1 G)^+ = {}
theorem irrefl_tranclI':
r^-1 Int r^+ = {} ==> ALL x. (x, x) ~: r^+
theorem subint1_irrefl:
[| (x, y) : subint1 G; ws_prog G |] ==> x ~= y
theorem subcls1_irrefl:
[| (x, y) : subcls1 G; ws_prog G |] ==> x ~= y
theorem subint1_acyclic:
ws_prog G ==> acyclic (subint1 G)
theorem subcls1_acyclic:
ws_prog G ==> acyclic (subcls1 G)
theorem wf_subint1:
ws_prog G ==> wf ((subint1 G)^-1)
theorem wf_subcls1:
ws_prog G ==> wf ((subcls1 G)^-1)
theorem subint1_induct:
[| ws_prog G; !!x. ALL y. (x, y) : subint1 G --> P y ==> P x |] ==> P a
theorem subcls1_induct:
[| ws_prog G; !!x. ALL y. (x, y) : subcls1 G --> P y ==> P x |] ==> P a
theorem wf_subint_:
ws_prog G ==> wf (((subint1 G)^+)^-1)
theorem wf_subcls_:
ws_prog G ==> wf (((subcls1 G)^+)^-1)
theorem ws_subint1_induct:
[| is_iface G I; ws_prog G;
!!I is ms.
iface G I = Some (is, ms) &
(ALL J:set is. (I, J) : subint1 G & P J & is_iface G J)
==> P I |]
==> P I
theorem ws_subcls1_induct:
[| is_class G C; ws_prog G;
!!C D si fs ms ini.
class G C = Some (D, si, fs, ms, ini) &
(C ~= Object --> (C, D) : subcls1 G & P D & is_class G D)
==> P C |]
==> P C
theorem ws_wfrel_lemma:
(!!G. ws_prog G ==> wf ((Rf G)^-1)) ==> wf (ws_wfrel Rf)
theorem wf_iface_wfrel:
wf (ws_wfrel subint1)
theorem wf_class_wfrel:
wf (ws_wfrel subcls1)
theorem iface_rec:
[| iface G I = Some (si, ib); ws_prog G |] ==> iface_rec (G, I) f = f I ib ((%J. iface_rec (G, J) f) `` set si)
theorem class_rec:
[| class G C = Some (sc, si, cb); ws_prog G |]
==> class_rec (G, C) t f =
f C cb (if C = Object then t else class_rec (G, sc) t f)
theorem imethds_rec:
[| iface G I = Some (is, ms); ws_prog G |]
==> imethds G I =
Un_tables (imethds G `` set is) \<oplus>\<oplus>
(o2s o table_of (map (%(s, mh). (s, I, mh)) ms))
theorem imethds_norec:
[| iface G md = Some (is, ms); ws_prog G; table_of ms sig = Some mh |] ==> (md, mh) : imethds G md sig
theorem imethds_defpl:
[| (md, mh) : imethds G I sig; ws_prog G; is_iface G I |]
==> (EX is ms. iface G md = Some (is, ms) & table_of ms sig = Some mh) &
(I, md) : (subint1 G)^* & (md, mh) : imethds G md sig
theorem cmethd_rec:
[| class G C = Some (sc, si, fs, ms, ini); ws_prog G |]
==> cmethd G C =
(if C = Object then empty else cmethd G sc) ++
table_of (map (%(s, m). (s, C, m)) ms)
theorem cmethd_norec:
[| class G md = Some (D, si, fs, ms, ini); ws_prog G;
table_of ms sig = Some m |]
==> cmethd G md sig = Some (md, m)
theorem cmethd_defpl:
[| cmethd G C sig = Some (md, m); ws_prog G; is_class G C |]
==> (EX D si fs ms ini.
class G md = Some (D, si, fs, ms, ini) & table_of ms sig = Some m) &
(C, md) : (subcls1 G)^* & cmethd G md sig = Some (md, m)
theorem finite_cmethd:
ws_prog G ==> finite {cmethd G C sig |sig C. is_class G C}
theorem finite_dom_cmethd:
[| ws_prog G; is_class G C |] ==> finite (dom (cmethd G C))
theorem fields_rec:
[| class G C = Some (sc, si, fs, ms, ini); ws_prog G |]
==> fields G C =
map (split (%fn. Pair (fn, C))) fs @
(if C = Object then [] else fields G sc)
theorem fields_norec:
[| class G fd = Some (D, si, fs, ms, ini); ws_prog G; table_of fs fn = Some f |] ==> table_of (fields G fd) (fn, fd) = Some f
theorem fields_defpl:
[| table_of (fields G C) (fn, fd) = Some f; ws_prog G; is_class G C |]
==> (EX D si fs ms ini.
class G fd = Some (D, si, fs, ms, ini) & table_of fs fn = Some f) &
(C, fd) : (subcls1 G)^* & table_of (fields G fd) (fn, fd) = Some f
theorem fields_emptyI:
[| ws_prog G; class G C = Some (sc, is, [], m, c);
C ~= Object --> class G sc = Some y & fields G sc = [] |]
==> fields G C = []
theorem fields_mono_lemma:
[| x : set (fields G C); (D, C) : (subcls1 G)^*; ws_prog G |] ==> x : set (fields G D)
theorem ws_unique_fields_lemma:
[| ((fn, C), f1) : set (fields G D); (fn, f2) : set fs; ws_prog G;
class G C = Some (D, si, fs, m_i); C ~= Object; class G D = Some c |]
==> R
theorem ws_unique_fields:
[| is_class G C; ws_prog G;
!!C D s fs r. class G C = Some (D, s, fs, r) ==> unique fs |]
==> unique (fields G C)
theorem cfield_fields:
cfield G C fn = Some (fd, fT) ==> table_of (fields G C) (fn, fd) = Some fT
theorem cfield_defpl_is_class:
[| is_class G C; cfield G C en = Some (fd, b, fT); ws_prog G |] ==> is_class G fd
theorem is_methdI:
[| class G C = Some y; cmethd G C sig = Some b |] ==> is_methd G C sig
theorem is_methdD:
is_methd G C sig ==> is_class G C & cmethd G C sig ~= None
theorem finite_is_methd:
ws_prog G ==> finite (Collect (split (is_methd G)))