(* Title: HOL/Bali/DeclConcepts.thy Author: Norbert Schirmer
*)
subsection \<open>Advanced concepts on Java declarations like overriding, inheritance,
dynamic method lookup\<close>
theory DeclConcepts imports TypeRel begin
subsubsection "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)"
definition is_public :: "prog \ qtname \ bool" where "is_public G qn = (case class G qn of
None \<Rightarrow> (case iface G qn of
None \<Rightarrow> False
| Some i \<Rightarrow> access i = Public)
| Some c \<Rightarrow> access c = Public)"
subsection "accessibility of types (cf. 6.6.1)" text\<open>
Primitive types are always accessible, interfaces andclasses are accessible in their package or if they are defined public, an array type is accessible if
its element type is accessible\<close>
definition
is_acc_class :: "prog \ pname \ qtname \ bool" where"is_acc_class G P C = (is_class G C \ G\(Class C) accessible_in P)"
definition
is_acc_iface :: "prog \ pname \ qtname \ bool" where"is_acc_iface G P I = (is_iface G I \ G\(Iface I) accessible_in P)"
definition
is_acc_type :: "prog \ pname \ ty \ bool" where"is_acc_type G P T = (is_type G T \ G\T accessible_in P)"
definition
is_acc_reftype :: "prog \ pname \ ref_ty \ bool" where"is_acc_reftype G P T = (isrtype G T \ G\T accessible_in' P)"
lemma is_acc_classD: "is_acc_class G P C \ is_class G C \ G\(Class C) accessible_in P" by (simp add: is_acc_class_def)
lemma is_acc_class_is_class: "is_acc_class G P C \ is_class G C" by (auto simp add: is_acc_class_def)
lemma is_acc_ifaceD: "is_acc_iface G P I \ is_iface G I \ G\(Iface I) accessible_in P" by (simp add: is_acc_iface_def)
lemma is_acc_typeD: "is_acc_type G P T \ is_type G T \ G\T accessible_in P" by (simp add: is_acc_type_def)
lemma is_acc_reftypeD: "is_acc_reftype G P T \ isrtype G T \ G\T accessible_in' P" by (simp add: is_acc_reftype_def)
subsection "accessibility of members" text\<open>
The accessibility of members is more involved as the accessibility of types.
We haveto distinguish several cases to model the different effects of
accessibility during inheritance, overriding and ordinary member access \<close>
subsubsection \<open>Various technical conversion and selection functions\<close>
text\<open>overloaded selector \<open>accmodi\<close> to select the access modifier
out of various HOL types\<close>
class has_accmodi = fixes accmodi:: "'a \ acc_modi"
lemma memberdecl_is_static_mdecl_simp[simp]: "is_static (mdecl m) = is_static m" by (simp add: memberdecl_is_static_def)
lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m" by (cases m) (simp add: mhead_def member_is_static_simp)
\<comment> \<open>some mnemotic selectors for various pairs\<close>
definition
decliface :: "qtname \ 'a decl_scheme \ qtname" where "decliface = fst"\<comment> \<open>get the interface component\<close>
definition
mbr :: "qtname \ memberdecl \ memberdecl" where "mbr = snd"\<comment> \<open>get the memberdecl component\<close>
definition
mthd :: "'b \ 'a \ 'a" where "mthd = snd"\<comment> \<open>get the method component\<close> \<comment> \<open>also used for mdecl, mhead\<close>
definition
fld :: "'b \ 'a decl_scheme \ 'a decl_scheme" where "fld = snd"\<comment> \<open>get the field component\<close> \<comment> \<open>also used for \<open>((vname \<times> qtname)\<times> field)\<close>\<close>
\<comment> \<open>some mnemotic selectors for \<open>(vname \<times> qtname)\<close>\<close>
definition
fname:: "vname \ 'a \ vname" where"fname = fst" \<comment> \<open>also used for fdecl\<close>
text\<open>Convert a qualified method declaration (qualified with its declaring class) to a qualified member declaration: \<open>methdMembr\<close>\<close>
definition
methdMembr :: "qtname \ mdecl \ qtname \ memberdecl" where"methdMembr m = (fst m, mdecl (snd m))"
lemma qmdecl_resTy_simp [simp]: "resTy (qmdecl sig m) = resTy m" by (cases m) (simp)
lemma resTy_mthd [simp]:"resTy (mthd m) = resTy m" by (cases m) (simp add: mthd_def )
subsubsection "inheritable-in" text\<open> \<open>G\<turnstile>m inheritable_in P\<close>: m can be inherited by classesin package P if: \begin{itemize} \item the declaration class of m is accessible in P and \item the member m is declared with protected or public access or if it is
declared with default (package) access, the package of the declaration class of m isalso P. If the member m is declared with private access
it is not accessible for inheritance at all. \end{itemize} \<close> definition
inheritable_in :: "prog \ (qtname \ memberdecl) \ pname \ bool" (\_ \ _ inheritable'_in _\ [61,61,61] 60) where "G\membr inheritable_in pack =
(case (accmodi membr) of
Private \<Rightarrow> False
| Package \<Rightarrow> (pid (declclass membr)) = pack
| Protected \<Rightarrow> True
| Public \<Rightarrow> True)"
abbreviation
Method_inheritable_in_syntax:: "prog \ (qtname \ mdecl) \ pname \ bool"
(\<open>_ \<turnstile>Method _ inheritable'_in _ \<close> [61,61,61] 60) where"G\Method m inheritable_in p == G\methdMembr m inheritable_in p"
abbreviation
Methd_inheritable_in:: "prog \ sig \ (qtname \ methd) \ pname \ bool"
(\<open>_ \<turnstile>Methd _ _ inheritable'_in _ \<close> [61,61,61,61] 60) where"G\Methd s m inheritable_in p == G\(method s m) inheritable_in p"
subsubsection "declared-in/undeclared-in"
definition
cdeclaredmethd :: "prog \ qtname \ (sig,methd) table" where "cdeclaredmethd G C =
(caseclass G C of
None \<Rightarrow> \<lambda> sig. None
| Some c \<Rightarrow> table_of (methods c))"
definition
cdeclaredfield :: "prog \ qtname \ (vname,field) table" where "cdeclaredfield G C =
(caseclass G C of
None \<Rightarrow> \<lambda> sig. None
| Some c \<Rightarrow> table_of (cfields c))"
definition
declared_in :: "prog \ memberdecl \ qtname \ bool" (\_\ _ declared'_in _\ [61,61,61] 60) where "G\m declared_in C = (case m of
fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn = Some f
| mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)"
abbreviation
method_declared_in:: "prog \ (qtname \ mdecl) \ qtname \ bool"
(\<open>_\<turnstile>Method _ declared'_in _\<close> [61,61,61] 60) where"G\Method m declared_in C == G\mdecl (mthd m) declared_in C"
abbreviation
methd_declared_in:: "prog \ sig \(qtname \ methd) \ qtname \ bool"
(\<open>_\<turnstile>Methd _ _ declared'_in _\<close> [61,61,61,61] 60) where"G\Methd s m declared_in C == G\mdecl (s,mthd m) declared_in C"
lemma declared_in_classD: "G\m declared_in C \ is_class G C" by (cases m)
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)
definition
undeclared_in :: "prog \ memberid \ qtname \ bool" (\_\ _ undeclared'_in _\ [61,61,61] 60) where "G\m undeclared_in C = (case m of
fid fn \<Rightarrow> cdeclaredfield G C fn = None
| mid sig \<Rightarrow> cdeclaredmethd G C sig = None)"
subsubsection "members"
(* Can't just take a function: prog \<Rightarrow> qtname \<Rightarrow> memberdecl set because the class qtname changes to the superclass in the inductive definition below
*)
inductive
members :: "prog \ (qtname \ memberdecl) \ qtname \ bool"
(\<open>_ \<turnstile> _ member'_of _\<close> [61,61,61] 60) for G :: prog where
Immediate: "\G\mbr m declared_in C;declclass m = C\ \ G\m member_of C"
| Inherited: "\G\m inheritable_in (pid C); G\memberid m undeclared_in C;
G\<turnstile>C \<prec>\<^sub>C1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S \<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C" text\<open>Note that in the case of an inherited member only the members of the
direct superclass are concerned. If a member of a superclass of the direct
superclass isn't inherited in the direct superclass (not member of the
direct superclass) than it can't be a member of the class. E.g. If a
member of a class A is defined with package access it isn't member of a subclass S if S isn't in the same package as A. Any further subclasses
of S will not inherit the member, regardless if they are in the same
package as A or not.\<close>
abbreviation
method_member_of:: "prog \ (qtname \ mdecl) \ qtname \ bool"
(\<open>_ \<turnstile>Method _ member'_of _\<close> [61,61,61] 60) where"G\Method m member_of C == G\(methdMembr m) member_of C"
abbreviation
methd_member_of:: "prog \ sig \ (qtname \ methd) \ qtname \ bool"
(\<open>_ \<turnstile>Methd _ _ member'_of _\<close> [61,61,61,61] 60) where"G\Methd s m member_of C == G\(method s m) member_of C"
abbreviation
fieldm_member_of:: "prog \ vname \ (qtname \ field) \ qtname \ bool"
(\<open>_ \<turnstile>Field _ _ member'_of _\<close> [61,61,61] 60) where"G\Field n f member_of C == G\fieldm n f member_of C"
definition
inherits :: "prog \ qtname \ (qtname \ memberdecl) \ bool" (\_ \ _ inherits _\ [61,61,61] 60) where "G\C inherits m =
(G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and>
(\<exists>S. G\<turnstile>C \<prec>\<^sub>C1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S))"
lemma inherits_member: "G\C inherits m \ G\m member_of C" by (auto simp add: inherits_def intro: members.Inherited)
definition
member_in :: "prog \ (qtname \ memberdecl) \ qtname \ bool" (\_ \ _ member'_in _\[61,61,61] 60) where"G\m member_in C = (\ provC. G\ C \\<^sub>C provC \ G \ m member_of provC)" text\<open>A member is in a class if it is member of the class or a superclass. If a member isin a class we can select this member. This additional notion is necessary since not all members are inherited to subclasses. So such
members are not member-of the subclass but member-in the subclass.\<close>
abbreviation
method_member_in:: "prog \ (qtname \ mdecl) \ qtname \ bool"
(\<open>_ \<turnstile>Method _ member'_in _\<close> [61,61,61] 60) where"G\Method m member_in C == G\(methdMembr m) member_in C"
abbreviation
methd_member_in:: "prog \ sig \ (qtname \ methd) \ qtname \ bool"
(\<open>_ \<turnstile>Methd _ _ member'_in _\<close> [61,61,61,61] 60) where"G\Methd s m member_in C == G\(method s m) member_in C"
lemma member_inD: "G\m member_in C \<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC" by (auto simp add: member_in_def)
lemma member_inI: "\G \ m member_of provC;G\ C \\<^sub>C provC\ \ G\m member_in C" by (auto simp add: member_in_def)
lemma member_of_to_member_in: "G \ m member_of C \ G \m member_in C" by (auto intro: member_inI)
subsubsection "overriding"
text\<open>Unfortunately the static notion of overriding (used during the
typecheck of the compiler) and the dynamic notion of overriding (used during
execution in the JVM) are not exactly the same. \<close>
text\<open>Static overriding (used during the typecheck of the compiler)\<close>
inductive
stat_overridesR :: "prog \ (qtname \ mdecl) \ (qtname \ mdecl) \ bool"
(\<open>_ \<turnstile> _ overrides\<^sub>S _\<close> [61,61,61] 60) for G :: prog where
Direct: "\\ is_static new; msig new = msig old;
G\<turnstile>Method new declared_in (declclass new);
G\<turnstile>Method old declared_in (declclass old);
G\<turnstile>Method old inheritable_in pid (declclass new);
G\<turnstile>(declclass new) \<prec>\<^sub>C1 superNew;
G \<turnstile>Method old member_of superNew \<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old"
subsubsection "permits access" definition
permits_acc :: "prog \ (qtname \ memberdecl) \ qtname \ qtname \ bool" (\_ \ _ in _ permits'_acc'_from _\ [61,61,61,61] 60) where "G\membr in cls permits_acc_from accclass =
(case (accmodi membr) of
Private \<Rightarrow> (declclass membr = accclass)
| Package \<Rightarrow> (pid (declclass membr) = pid accclass)
| Protected \<Rightarrow> (pid (declclass membr) = pid accclass) \<or>
(G\<turnstile>accclass \<prec>\<^sub>C declclass membr \<and> (G\<turnstile>cls \<preceq>\<^sub>C accclass \<or> is_static membr))
| Public \<Rightarrow> True)" text\<open>
The subcondition of the \<^term>\<open>Protected\<close> case: \<^term>\<open>G\<turnstile>accclass \<prec>\<^sub>C declclass membr\<close> could also be relaxed to: \<^term>\<open>G\<turnstile>accclass \<preceq>\<^sub>C declclass membr\<close> since in case both classes are the
same the other condition \<^term>\<open>(pid (declclass membr) = pid accclass)\<close>
holds anyway. \<close>
text\<open>Like in case of overriding, the static and dynamic accessibility
of members is not uniform. \begin{itemize} \item Statically the class/interface of the member must be accessible for the
member to be accessible. During runtime this is not necessary. For
Example, if a classis accessible and we are allowed to access a member
of this class (statically) we expect that we can access this member in
an arbitrary subclass (during runtime). It's not intended to restrict
the access to accessible subclasses during runtime. \item Statically the member we want to access must be "member of" the class.
Dynamically it must only be "member in" the class. \end{itemize} \<close>
inductive
accessible_fromR :: "prog \ qtname \ (qtname \ memberdecl) \ qtname \ bool" and accessible_from :: "prog \ (qtname \ memberdecl) \ qtname \ qtname \ bool"
(\<open>_ \<turnstile> _ of _ accessible'_from _\<close> [61,61,61,61] 60) and method_accessible_from :: "prog \ (qtname \ mdecl) \ qtname \ qtname \ bool"
(\<open>_ \<turnstile>Method _ of _ accessible'_from _\<close> [61,61,61,61] 60) for G :: prog and accclass :: qtname where "G\membr of cls accessible_from accclass \ accessible_fromR G accclass membr cls"
| "G\Method m of cls accessible_from accclass \ accessible_fromR G accclass (methdMembr m) cls"
| Immediate: "!!membr class. \<lbrakk>G\<turnstile>membr member_of class;
G\<turnstile>(Class class) accessible_in (pid accclass);
G\<turnstile>membr in class permits_acc_from accclass \<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
| Overriding: "!!membr class C new old supr. \<lbrakk>G\<turnstile>membr member_of class;
G\<turnstile>(Class class) accessible_in (pid accclass);
membr=(C,mdecl new);
G\<turnstile>(C,new) overrides\<^sub>S old;
G\<turnstile>class \<prec>\<^sub>C supr;
G\<turnstile>Method old of supr accessible_from accclass \<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass"
abbreviation
methd_accessible_from:: "prog \ sig \ (qtname \ methd) \ qtname \ qtname \ bool"
(\<open>_ \<turnstile>Methd _ _ of _ accessible'_from _\<close> [61,61,61,61,61] 60) where "G\Methd s m of cls accessible_from accclass ==
G\<turnstile>(method s m) of cls accessible_from accclass"
abbreviation
field_accessible_from:: "prog \ vname \ (qtname \ field) \ qtname \ qtname \ bool"
(\<open>_ \<turnstile>Field _ _ of _ accessible'_from _\<close> [61,61,61,61,61] 60) where "G\Field fn f of C accessible_from accclass ==
G\<turnstile>(fieldm fn f) of C accessible_from accclass"
inductive
dyn_accessible_fromR :: "prog \ qtname \ (qtname \ memberdecl) \ qtname \ bool" and dyn_accessible_from' :: "prog \ (qtname \ memberdecl) \ qtname \ qtname \ bool"
(\<open>_ \<turnstile> _ in _ dyn'_accessible'_from _\<close> [61,61,61,61] 60) and method_dyn_accessible_from :: "prog \ (qtname \ mdecl) \ qtname \ qtname \ bool"
(\<open>_ \<turnstile>Method _ in _ dyn'_accessible'_from _\<close> [61,61,61,61] 60) for G :: prog and accclass :: qtname where "G\membr in C dyn_accessible_from accC \ dyn_accessible_fromR G accC membr C"
| "G\Method m in C dyn_accessible_from accC \ dyn_accessible_fromR G accC (methdMembr m) C"
| Immediate: "!!class. \G\membr member_in class;
G\<turnstile>membr in class permits_acc_from accclass \<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
| Overriding: "!!class. \G\membr member_in class;
membr=(C,mdecl new);
G\<turnstile>(C,new) overrides old;
G\<turnstile>class \<prec>\<^sub>C supr;
G\<turnstile>Method old in supr dyn_accessible_from accclass \<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass"
abbreviation
methd_dyn_accessible_from:: "prog \ sig \ (qtname \ methd) \ qtname \ qtname \ bool"
(\<open>_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _\<close> [61,61,61,61,61] 60) where "G\Methd s m in C dyn_accessible_from accC ==
G\<turnstile>(method s m) in C dyn_accessible_from accC"
abbreviation
field_dyn_accessible_from:: "prog \ vname \ (qtname \ field) \ qtname \ qtname \ bool"
(\<open>_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _\<close> [61,61,61,61,61] 60) where "G\Field fn f in dynC dyn_accessible_from accC ==
G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC"
lemma accessible_from_commonD: "G\m of C accessible_from S \<Longrightarrow> G\<turnstile>m member_of C \<and> G\<turnstile>(Class C) accessible_in (pid S)" by (auto elim: accessible_fromR.induct)
lemma unique_declaration: "\G\m declared_in C; G\n declared_in C; memberid m = memberid n \ \<Longrightarrow> m = n" apply (cases m) apply (cases n,
auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+ done
lemma declared_not_undeclared: "G\m declared_in C \ \ G\ memberid m undeclared_in C" by (cases m) (auto simp add: declared_in_def undeclared_in_def)
lemma undeclared_not_declared: "G\ memberid m undeclared_in C \ \ G\ m declared_in C" by (cases m) (auto simp add: declared_in_def undeclared_in_def)
lemma not_undeclared_declared: "\ G\ membr_id undeclared_in C \ (\ m. G\m declared_in C \
membr_id = memberid m)" proof - assume not_undecl:"\ G\ membr_id undeclared_in C" show ?thesis (is"?P membr_id") proof (cases membr_id) case (fid vname) with not_undecl obtain fld where "G\fdecl (vname,fld) declared_in C" by (auto simp add: undeclared_in_def declared_in_def
cdeclaredfield_def) with fid show ?thesis by auto next case (mid sig) with not_undecl obtain mthd where "G\mdecl (sig,mthd) declared_in C" by (auto simp add: undeclared_in_def declared_in_def
cdeclaredmethd_def) with mid show ?thesis by auto qed qed
lemma unique_declared_in: "\G\m declared_in C; G\n declared_in C; memberid m = memberid n\ \<Longrightarrow> m = n" by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def
split: memberdecl.splits)
lemma unique_member_of: assumes n: "G\n member_of C" and
m: "G\m member_of C" and
eqid: "memberid n = memberid m" shows"n=m" proof - from n m eqid show"n=m" proof (induct) case (Immediate n C) assume member_n: "G\ mbr n declared_in C" "declclass n = C" assume eqid: "memberid n = memberid m" assume"G \ m member_of C" thenshow"n=m" proof (cases) case Immediate with eqid member_n show ?thesis by (cases n, cases m)
(auto simp add: declared_in_def
cdeclaredmethd_def cdeclaredfield_def
split: memberdecl.splits) next case Inherited with eqid member_n show ?thesis by (cases n) (auto dest: declared_not_undeclared) qed next case (Inherited n C S) assume undecl: "G\ memberid n undeclared_in C" assume super: "G\C\\<^sub>C1S" assume hyp: "\G \ m member_of S; memberid n = memberid m\ \ n = m" assume eqid: "memberid n = memberid m" assume"G \ m member_of C" thenshow"n=m" proof (cases) case Immediate thenhave"G\ mbr m declared_in C" by simp with eqid undecl show ?thesis by (cases m) (auto dest: declared_not_undeclared) next case Inherited with super have"G \ m member_of S" by (auto dest!: subcls1D) with eqid hyp show ?thesis by blast qed qed qed
lemma member_of_is_classD: "G\m member_of C \ is_class G C" proof (induct set: members) case (Immediate m C) assume"G\ mbr m declared_in C" thenshow"is_class G C" by (cases "mbr m")
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def) next case (Inherited m C S) show"is_class G C"if"G\C\\<^sub>C1S" and "is_class G S" by (rule subcls_is_class2) (use that in auto) qed
lemma member_of_declC: "G\m member_of C \<Longrightarrow> G\<turnstile>mbr m declared_in (declclass m)" by (induct set: members) auto
lemma member_of_member_of_declC: "G\m member_of C \<Longrightarrow> G\<turnstile>m member_of (declclass m)" by (auto dest: member_of_declC intro: members.Immediate)
lemma member_of_class_relation: "G\m member_of C \ G\C \\<^sub>C declclass m" proof (induct set: members) case (Immediate m C) thenshow"G\C \\<^sub>C declclass m" by simp next case (Inherited m C S) thenshow"G\C \\<^sub>C declclass m" by (auto dest: r_into_rtrancl intro: rtrancl_trans) qed
lemma member_in_class_relation: "G\m member_in C \ G\C \\<^sub>C declclass m" by (auto dest: member_inD member_of_class_relation
intro: rtrancl_trans)
lemma stat_overrides_commonD: "\G\new overrides\<^sub>S old\ \
declclass new \<noteq> Object \<and> \<not> is_static new \<and> msig new = msig old \<and>
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and>
G\<turnstile>Method new declared_in (declclass new) \<and>
G\<turnstile>Method old declared_in (declclass old)" apply (induct set: stat_overridesR) apply (frule (1) stat_override_declclasses_relation) apply (auto intro: trancl_trans) done
lemma member_of_Package: assumes"G\m member_of C" and"accmodi m = Package" shows"pid (declclass m) = pid C" using assms proof induct case Immediate thenshow ?caseby simp next case Inherited thenshow ?caseby (auto simp add: inheritable_in_def) qed
lemma member_in_declC: "G\m member_in C\ G\m member_in (declclass m)" proof - assume member_in_C: "G\m member_in C" from member_in_C obtain provC where
subclseq_C_provC: "G\ C \\<^sub>C provC" and
member_of_provC: "G \ m member_of provC" by (auto simp add: member_in_def) from member_of_provC have"G \ m member_of declclass m" by (rule member_of_member_of_declC) moreover from member_in_C have"G\C \\<^sub>C declclass m" by (rule member_in_class_relation) ultimately show ?thesis by (auto simp add: member_in_def) qed
lemma dyn_accessible_from_commonD: "G\m in C dyn_accessible_from S \<Longrightarrow> G\<turnstile>m member_in C" by (auto elim: dyn_accessible_fromR.induct)
lemma no_Private_stat_override: "\G\new overrides\<^sub>S old\ \ accmodi old \ Private" by (induct set: stat_overridesR) (auto simp add: inheritable_in_def)
lemma no_Private_override: "\G\new overrides old\ \ accmodi old \ Private" by (induct set: overridesR) (auto simp add: inheritable_in_def)
lemma permits_acc_inheritance: "\G\m in statC permits_acc_from accC; G\dynC \\<^sub>C statC \<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_from accC" by (cases "accmodi m")
(auto simp add: permits_acc_def
intro: subclseq_trans)
lemma permits_acc_static_declC: "\G\m in C permits_acc_from accC; G\m member_in C; is_static m \<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_from accC" by (cases "accmodi m") (auto simp add: permits_acc_def)
lemma dyn_accessible_from_static_declC: assumes acc_C: "G\m in C dyn_accessible_from accC" and
static: "is_static m" shows"G\m in (declclass m) dyn_accessible_from accC" proof - from acc_C static show"G\m in (declclass m) dyn_accessible_from accC" proof (induct) case (Immediate m C) thenshow ?case by (auto intro!: dyn_accessible_fromR.Immediate
dest: member_in_declC permits_acc_static_declC) next case (Overriding m C declCNew new old sup) thenhave"\ is_static m" by (auto dest: overrides_commonD) moreover assume"is_static m" ultimatelyshow ?case by contradiction qed qed
lemma field_accessible_fromD: "\G\membr of C accessible_from accC;is_field membr\ \<Longrightarrow> G\<turnstile>membr member_of C \<and>
G\<turnstile>(Class C) accessible_in (pid accC) \<and>
G\<turnstile>membr in C permits_acc_from accC" by (cases set: accessible_fromR)
(auto simp add: is_field_def split: memberdecl.splits)
lemma field_accessible_from_permits_acc_inheritance: "\G\membr of statC accessible_from accC; is_field membr; G \ dynC \\<^sub>C statC\ \<Longrightarrow> G\<turnstile>membr in dynC permits_acc_from accC" by (auto dest: field_accessible_fromD intro: permits_acc_inheritance)
(* lemma accessible_Package: "\<lbrakk>G \<turnstile> m of C accessible_from S;accmodi m = Package; \<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new\<rbrakk> \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)" proof - assume wf: "\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new" assume "G \<turnstile> m of C accessible_from S" then show "accmodi m = Package \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)" (is "?Pack m \<Longrightarrow> ?P C m") proof (induct rule: accessible_fromR.induct) fix C m assume "G\<turnstile>m member_of C" "G \<turnstile> m in C permits_acc_from S" "accmodi m = Package" then show "?P C m" by (auto dest: member_of_Package simp add: permits_acc_def) next fix declC C new newm old Sup assume member_new: "G \<turnstile> new member_of C" and acc_C: "G \<turnstile> Class C accessible_in pid S" and new: "new = (declC, mdecl newm)" and override: "G \<turnstile> (declC, newm) overrides\<^sub>S old" and subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and acc_old: "G \<turnstile> methdMembr old of Sup accessible_from S" and hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P Sup (methdMembr old)" and accmodi_new: "accmodi new = Package" from override wf have accmodi_weaken: "accmodi old \<le> accmodi newm" by (cases old,cases newm) auto from override new have "accmodi old \<noteq> Private" by (simp add: no_Private_stat_override) with accmodi_weaken accmodi_new new have accmodi_old: "accmodi old = Package" by (cases "accmodi old") (auto simp add: le_acc_def less_acc_def) with hyp have P_sup: "?P Sup (methdMembr old)" by (simp) from wf override new accmodi_old accmodi_new have eq_pid_new_old: "pid (declclass new) = pid (declclass old)" by (auto dest: stat_override_Package) from member_new accmodi_new have "pid (declclass new) = pid C" by (auto dest: member_of_Package) with eq_pid_new_old P_sup show "?P C new" by auto qed qed
*)
lemma accessible_fieldD: "\G\membr of C accessible_from accC; is_field membr\ \<Longrightarrow> G\<turnstile>membr member_of C \<and>
G\<turnstile>(Class C) accessible_in (pid accC) \<and>
G\<turnstile>membr in C permits_acc_from accC" by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD)
lemma member_of_Private: "\G\m member_of C; accmodi m = Private\ \ declclass m = C" by (induct set: members) (auto simp add: inheritable_in_def)
lemma member_of_subclseq_declC: "G\m member_of C \ G\C \\<^sub>C declclass m" by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans)
lemma member_of_inheritance: assumes m: "G\m member_of D" and
subclseq_D_C: "G\D \\<^sub>C C" and
subclseq_C_m: "G\C \\<^sub>C declclass m" and
ws: "ws_prog G" shows"G\m member_of C" proof - from m subclseq_D_C subclseq_C_m show ?thesis proof (induct) case (Immediate m D) assume"declclass m = D"and "G\D\\<^sub>C C" and "G\C\\<^sub>C declclass m" with ws have"D=C" by (auto intro: subclseq_acyclic) with Immediate show"G\m member_of C" by (auto intro: members.Immediate) next case (Inherited m D S) assume member_of_D_props: "G \ m inheritable_in pid D" "G\ memberid m undeclared_in D" "G \ Class S accessible_in pid D" "G \ m member_of S" assume super: "G\D\\<^sub>C1S" assume hyp: "\G\S\\<^sub>C C; G\C\\<^sub>C declclass m\ \ G \ m member_of C" assume subclseq_C_m: "G\C\\<^sub>C declclass m" assume"G\D\\<^sub>C C" thenshow"G\m member_of C" proof (cases rule: subclseq_cases) case Eq assume"D=C" with super member_of_D_props show ?thesis by (auto intro: members.Inherited) next case Subcls assume"G\D\\<^sub>C C" with super have"G\S\\<^sub>C C" by (auto dest: subcls1D subcls_superD) with subclseq_C_m hyp show ?thesis by blast qed qed qed
lemma member_of_subcls: assumes old: "G\old member_of C" and
new: "G\new member_of D" and
eqid: "memberid new = memberid old"and
subclseq_D_C: "G\D \\<^sub>C C" and
subcls_new_old: "G\declclass new \\<^sub>C declclass old" and
ws: "ws_prog G" shows"G\D \\<^sub>C C" proof - from old have subclseq_C_old: "G\C \\<^sub>C declclass old" by (auto dest: member_of_subclseq_declC) from new have subclseq_D_new: "G\D \\<^sub>C declclass new" by (auto dest: member_of_subclseq_declC) from subcls_new_old ws have neq_new_old: "new\old" by (cases new,cases old) (auto dest: subcls_irrefl) from subclseq_D_new subclseq_D_C have"G\(declclass new) \\<^sub>C C \ G\C \\<^sub>C (declclass new)" by (rule subcls_compareable) thenhave"G\(declclass new) \\<^sub>C C" proof assume"G\declclass new\\<^sub>C C" then show ?thesis . next assume"G\C \\<^sub>C (declclass new)" with new subclseq_D_C ws have"G\new member_of C" by (blast intro: member_of_inheritance) with eqid old have"new=old" by (blast intro: unique_member_of) with neq_new_old show ?thesis by contradiction qed thenshow ?thesis proof (cases rule: subclseq_cases) case Eq assume"declclass new = C" with new have"G\new member_of C" by (auto dest: member_of_member_of_declC) with eqid old have"new=old" by (blast intro: unique_member_of) with neq_new_old show ?thesis by contradiction next case Subcls assume"G\declclass new\\<^sub>C C" with subclseq_D_new show"G\D\\<^sub>C C" by (rule rtrancl_trancl_trancl) qed qed
corollary member_of_overrides_subcls: "\G\Methd sig old member_of C; G\Methd sig new member_of D;G\D \\<^sub>C C;
G,sig\<turnstile>new overrides old; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C" by (drule overrides_commonD) (auto intro: member_of_subcls)
corollary member_of_stat_overrides_subcls: "\G\Methd sig old member_of C; G\Methd sig new member_of D;G\D \\<^sub>C C;
G,sig\<turnstile>new overrides\<^sub>S old; ws_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C" by (drule stat_overrides_commonD) (auto intro: member_of_subcls)
lemma inherited_field_access: assumes stat_acc: "G\membr of statC accessible_from accC" and
is_field: "is_field membr"and
subclseq: "G \ dynC \\<^sub>C statC" shows"G\membr in dynC dyn_accessible_from accC" proof - from stat_acc is_field subclseq show ?thesis by (auto dest: accessible_fieldD
intro: dyn_accessible_fromR.Immediate
member_inI
permits_acc_inheritance) qed
lemma accessible_inheritance: assumes stat_acc: "G\m of statC accessible_from accC" and
subclseq: "G\dynC \\<^sub>C statC" and
member_dynC: "G\m member_of dynC" and
dynC_acc: "G\(Class dynC) accessible_in (pid accC)" shows"G\m of dynC accessible_from accC" proof - from stat_acc have member_statC: "G\m member_of statC" by (auto dest: accessible_from_commonD) from stat_acc show ?thesis proof (cases) case Immediate with member_dynC member_statC subclseq dynC_acc show ?thesis by (auto intro: accessible_fromR.Immediate permits_acc_inheritance) next case Overriding with member_dynC subclseq dynC_acc show ?thesis by (auto intro: accessible_fromR.Overriding rtrancl_trancl_trancl) qed qed
definition
imethds :: "prog \ qtname \ (sig,qtname \ mhead) tables" where "imethds G I =
iface_rec G I (\<lambda>I i ts. (Un_tables ts) \<oplus>\<oplus>
(set_option \<circ> table_of (map (\<lambda>(s,m). (s,I,m)) (imethods i))))" text\<open>methods of an interface, with overriding and inheritance, cf. 9.2\<close>
definition
accimethds :: "prog \ pname \ qtname \ (sig,qtname \ mhead) tables" where "accimethds G pack I =
(if G\<turnstile>Iface I accessible_in pack then imethds G I
else (\<lambda> k. {}))" text\<open>only returns imethds if the interface is accessible\<close>
definition
methd :: "prog \ qtname \ (sig,qtname \ methd) table" where "methd G C =
class_rec G C Map.empty
(\<lambda>C c subcls_mthds.
filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
subcls_mthds
++
table_of (map (\<lambda>(s,m). (s,C,m)) (methods c)))" text\<open>\<^term>\<open>methd G C\<close>: methods of a class C (statically visible from C), with inheritance and hiding cf. 8.4.6;
Overriding is captured by\<open>dynmethd\<close>.
Every new method with the same signature coalesces the
method of a superclass.\<close>
definition
accmethd :: "prog \ qtname \ qtname \ (sig,qtname \ methd) table" where "accmethd G S C =
filter_tab (\<lambda>sig m. G\<turnstile>method sig m of C accessible_from S) (methd G C)" text\<open>\<^term>\<open>accmethd G S C\<close>: only those methods of \<^term>\<open>methd G C\<close>,
accessible from S\<close>
text\<open>Note the class component in the accessibility filter. The class where
method \<^term>\<open>m\<close> is declared (\<^term>\<open>declC\<close>) isn't necessarily accessible from the current scope \<^term>\<open>S\<close>. The method can be made accessible
through inheritance, too.
So we must test accessibility of method \<^term>\<open>m\<close> of class \<^term>\<open>C\<close>
(not \<^term>\<open>declclass m\<close>)\<close>
definition
dynmethd :: "prog \ qtname \ qtname \ (sig,qtname \ methd) table" where "dynmethd G statC dynC =
(\<lambda>sig.
(if G\<turnstile>dynC \<preceq>\<^sub>C statC then (case methd G statC sig of
None \<Rightarrow> None
| Some statM \<Rightarrow> (class_rec G dynC Map.empty
(\<lambda>C c subcls_mthds.
subcls_mthds
++
(filter_tab
(\<lambda> _ dynM. G,sig\<turnstile>dynM overrides statM \<or> dynM=statM)
(methd G C) ))
) sig
)
else None))"
text\<open>\<^term>\<open>dynmethd G statC dynC\<close>: dynamic method lookup of a reference with dynamic class\<^term>\<open>dynC\<close> and static class \<^term>\<open>statC\<close>\<close> text\<open>Note some kind of duality between \<^term>\<open>methd\<close> and \<^term>\<open>dynmethd\<close> in the \<^term>\<open>class_rec\<close> arguments. Whereas \<^term>\<open>methd\<close> filters the subclass methods (to get only the inherited ones), \<^term>\<open>dynmethd\<close>
filters the new methods (to get only those methods which actually
override the methods of the static class)\<close>
definition
dynimethd :: "prog \ qtname \ qtname \ (sig,qtname \ methd) table" where "dynimethd G I dynC =
(\<lambda>sig. if imethds G I sig \<noteq> {} then methd G dynC sig
else dynmethd G Object dynC sig)" text\<open>\<^term>\<open>dynimethd G I dynC\<close>: dynamic method lookup of a reference with
dynamic class dynC and static interface type I\<close> text\<open>
When calling an interface method, we must distinguish if the method signature
was defined in the interface or if it must be an Object method in the other case. If it was an interface method we search the class hierarchy
starting at the dynamic class of the object up to Object to find the
first matching method (\<^term>\<open>methd\<close>). Since all interface methods have
public access the method can't be coalesced due to some odd visibility
effects like incase of dynmethd. The method will be inherited or
overridden in all classesfrom the first class implementing the interface
down to the actual dynamic class. \<close>
definition
dynlookup :: "prog \ ref_ty \ qtname \ (sig,qtname \ methd) table" where "dynlookup G statT dynC =
(case statT of
NullT \<Rightarrow> Map.empty
| IfaceT I \<Rightarrow> dynimethd G I dynC
| ClassT statC \<Rightarrow> dynmethd G statC dynC
| ArrayT ty \<Rightarrow> dynmethd G Object dynC)" text\<open>\<^term>\<open>dynlookup G statT dynC\<close>: dynamic lookup of a method within the
static reference type statT and the dynamic class dynC. In a wellformd context statT will not be NullT andincase
statT is an array type, dynC=Object\<close>
definition
fields :: "prog \ qtname \ ((vname \ qtname) \ field) list" where "fields G C =
class_rec G C [] (\<lambda>C c ts. map (\<lambda>(n,t). ((n,C),t)) (cfields c) @ ts)" text\<open>\<^term>\<open>fields G C\<close>
list of fields of a class, including all the fields of the superclasses
(private, inherited and hidden ones) not only the accessible ones
(an instance of a object allocates all these fields\<close>
definition
accfield :: "prog \ qtname \ qtname \ (vname, qtname \ field) table" where "accfield G S C =
(let field_tab = table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (fields G C)) in filter_tab (\<lambda>n (declC,f). G\<turnstile> (declC,fdecl (n,f)) of C accessible_from S)
field_tab)" text\<open>\<^term>\<open>accfield G C S\<close>: fields of a class \<^term>\<open>C\<close> which are
accessible from scope of class \<^term>\<open>S\<close> with inheritance and hiding, cf. 8.3\<close> text\<open>note the class component in the accessibility filter (see also \<^term>\<open>methd\<close>).
The class declaring field \<^term>\<open>f\<close> (\<^term>\<open>declC\<close>) isn't necessarily
accessible from scope \<^term>\<open>S\<close>. The field can be made visible through
inheritance, too. So we must test accessibility of field \<^term>\<open>f\<close> of class \<^term>\<open>C\<close> (not \<^term>\<open>declclass f\<close>)\<close>
definition
is_methd :: "prog \ qtname \ sig \ bool" where"is_methd G = (\C sig. is_class G C \ methd G C sig \ None)"
lemma efname_simp[simp]:"efname (n,f) = n" by (simp add: efname_def)
subsection "imethds"
lemma imethds_rec: "\iface G I = Some i; ws_prog G\ \
imethds G I = Un_tables ((\<lambda>J. imethds G J)`set (isuperIfs i)) \<oplus>\<oplus>
(set_option \<circ> table_of (map (\<lambda>(s,mh). (s,I,mh)) (imethods i)))" apply (unfold imethds_def) apply (rule iface_rec [THEN trans]) apply auto done
(* local lemma *) lemma imethds_norec: "\iface G md = Some i; ws_prog G; table_of (imethods i) sig = Some mh\ \
(md, mh) \<in> imethds G md sig" apply (subst imethds_rec) apply assumption+ apply (rule iffD2) apply (rule overrides_t_Some_iff) apply (rule disjI1) apply (auto elim: table_of_map_SomeI) done
lemma imethds_declI: "\m \ imethds G I sig; ws_prog G; is_iface G I\ \
(\<exists>i. iface G (decliface m) = Some i \<and>
table_of (imethods i) sig = Some (mthd m)) \<and>
(I,decliface m) \<in> (subint1 G)\<^sup>* \<and> m \<in> imethds G (decliface m) sig" apply (erule rev_mp) apply (rule ws_subint1_induct, assumption, assumption) apply (subst imethds_rec, erule conjunct1, assumption) apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2) done
lemma imethds_cases: assumes im: "im \ imethds G I sig" and ifI: "iface G I = Some i" and ws: "ws_prog G" obtains (NewMethod) "table_of (map (\(s, mh). (s, I, mh)) (imethods i)) sig = Some im"
| (InheritedMethod) J where"J \ set (isuperIfs i)" and "im \ imethds G J sig" using assms by (auto simp add: imethds_rec)
subsection "accimethd"
lemma accimethds_simp [simp]: "G\Iface I accessible_in pack \ accimethds G pack I = imethds G I" by (simp add: accimethds_def)
lemma accimethdsD: "im \ accimethds G pack I sig \<Longrightarrow> im \<in> imethds G I sig \<and> G\<turnstile>Iface I accessible_in pack" by (auto simp add: accimethds_def)
lemma accimethdsI: "\im \ imethds G I sig;G\Iface I accessible_in pack\ \<Longrightarrow> im \<in> accimethds G pack I sig" by simp
subsection "methd"
lemma methd_rec: "\class G C = Some c; ws_prog G\ \
methd G C
= (if C = Object then Map.empty
else filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)
(methd G (super c)))
++ table_of (map (\<lambda>(s,m). (s,C,m)) (methods c))" apply (unfold methd_def) apply (erule class_rec [THEN trans], assumption) apply (simp) done
(* local lemma *) lemma methd_norec: "\class G declC = Some c; ws_prog G;table_of (methods c) sig = Some m\ \<Longrightarrow> methd G declC sig = Some (declC, m)" apply (simp only: methd_rec) apply (rule disjI1 [THEN map_add_Some_iff [THEN iffD2]]) apply (auto elim: table_of_map_SomeI) done
lemma methd_declC: "\methd G C sig = Some m; ws_prog G;is_class G C\ \
(\<exists>d. class G (declclass m)=Some d \<and> table_of (methods d) sig=Some (mthd m)) \<and>
G\<turnstile>C \<preceq>\<^sub>C (declclass m) \<and> methd G (declclass m) sig = Some m" apply (erule rev_mp) apply (rule ws_subcls1_induct, assumption, assumption) apply (subst methd_rec, assumption) apply (case_tac "Ca=Object")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
