Theory WellForm
subsection ‹Well-formedness of Java programs›
theory WellForm imports DefiniteAssignment begin
text ‹
For static checks on expressions and statements, see WellType.thy
improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
\begin{itemize}
\item a method implementing or overwriting another method may have a result
type that widens to the result type of the other method
(instead of identical type)
\item if a method hides another method (both methods have to be static!)
there are no restrictions to the result type
since the methods have to be static and there is no dynamic binding of
static methods
\item if an interface inherits more than one method with the same signature, the
methods need not have identical return types
\end{itemize}
simplifications:
\begin{itemize}
\item Object and standard exceptions are assumed to be declared like normal
classes
\end{itemize}
›
subsubsection "well-formed field declarations"
text ‹well-formed field declaration (common part for classes and interfaces),
cf. 8.3 and (9.3)›
definition
wf_fdecl :: "prog ⇒ pname ⇒ fdecl ⇒ bool"
where "wf_fdecl G P = (λ(fn,f). is_acc_type G P (type f))"
lemma wf_fdecl_def2: "⋀fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
apply (unfold wf_fdecl_def)
apply simp
done
subsubsection "well-formed method declarations"
text ‹
A method head is wellformed if:
\begin{itemize}
\item the signature and the method head agree in the number of parameters
\item all types of the parameters are visible
\item the result type is visible
\item the parameter names are unique
\end{itemize}
›
definition
wf_mhead :: "prog ⇒ pname ⇒ sig ⇒ mhead ⇒ bool" where
"wf_mhead G P = (λ sig mh. length (parTs sig) = length (pars mh) ∧
( ∀T∈set (parTs sig). is_acc_type G P T) ∧
is_acc_type G P (resTy mh) ∧
distinct (pars mh))"
text ‹
A method declaration is wellformed if:
\begin{itemize}
\item the method head is wellformed
\item the names of the local variables are unique
\item the types of the local variables must be accessible
\item the local variables don't shadow the parameters
\item the class of the method is defined
\item the body statement is welltyped with respect to the
modified environment of local names, were the local variables,
the parameters the special result variable (Res) and This are assoziated
with there types.
\end{itemize}
›
definition
callee_lcl :: "qtname ⇒ sig ⇒ methd ⇒ lenv" where
"callee_lcl C sig m =
(λk. (case k of
EName e
⇒ (case e of
VNam v
⇒((table_of (lcls (mbody m)))(pars m [↦] parTs sig)) v
| Res ⇒ Some (resTy m))
| This ⇒ if is_static m then None else Some (Class C)))"
definition
parameters :: "methd ⇒ lname set" where
"parameters m = set (map (EName ∘ VNam) (pars m)) ∪ (if (static m) then {} else {This})"
definition
wf_mdecl :: "prog ⇒ qtname ⇒ mdecl ⇒ bool" where
"wf_mdecl G C =
(λ(sig,m).
wf_mhead G (pid C) sig (mhead m) ∧
unique (lcls (mbody m)) ∧
(∀(vn,T)∈set (lcls (mbody m)). is_acc_type G (pid C) T) ∧
(∀pn∈set (pars m). table_of (lcls (mbody m)) pn = None) ∧
jumpNestingOkS {Ret} (stmt (mbody m)) ∧
is_class G C ∧
⦇prg=G,cls=C,lcl=callee_lcl C sig m⦈⊢(stmt (mbody m))∷√ ∧
(∃ A. ⦇prg=G,cls=C,lcl=callee_lcl C sig m⦈
⊢ parameters m »⟨stmt (mbody m)⟩» A
∧ Result ∈ nrm A))"
lemma callee_lcl_VNam_simp [simp]:
"callee_lcl C sig m (EName (VNam v))
= ((table_of (lcls (mbody m)))(pars m [↦] parTs sig)) v"
by (simp add: callee_lcl_def)
lemma callee_lcl_Res_simp [simp]:
"callee_lcl C sig m (EName Res) = Some (resTy m)"
by (simp add: callee_lcl_def)
lemma callee_lcl_This_simp [simp]:
"callee_lcl C sig m (This) = (if is_static m then None else Some (Class C))"
by (simp add: callee_lcl_def)
lemma callee_lcl_This_static_simp:
"is_static m ⟹ callee_lcl C sig m (This) = None"
by simp
lemma callee_lcl_This_not_static_simp:
"¬ is_static m ⟹ callee_lcl C sig m (This) = Some (Class C)"
by simp
lemma wf_mheadI:
"⟦length (parTs sig) = length (pars m); ∀T∈set (parTs sig). is_acc_type G P T;
is_acc_type G P (resTy m); distinct (pars m)⟧ ⟹
wf_mhead G P sig m"
apply (unfold wf_mhead_def)
apply (simp (no_asm_simp))
done
lemma wf_mdeclI: "⟦
wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));
(∀pn∈set (pars m). table_of (lcls (mbody m)) pn = None);
∀(vn,T)∈set (lcls (mbody m)). is_acc_type G (pid C) T;
jumpNestingOkS {Ret} (stmt (mbody m));
is_class G C;
⦇prg=G,cls=C,lcl=callee_lcl C sig m⦈⊢(stmt (mbody m))∷√;
(∃ A. ⦇prg=G,cls=C,lcl=callee_lcl C sig m⦈ ⊢ parameters m »⟨stmt (mbody m)⟩» A
∧ Result ∈ nrm A)
⟧ ⟹
wf_mdecl G C (sig,m)"
apply (unfold wf_mdecl_def)
apply simp
done
lemma wf_mdeclE [consumes 1]:
"⟦wf_mdecl G C (sig,m);
⟦wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));
∀pn∈set (pars m). table_of (lcls (mbody m)) pn = None;
∀(vn,T)∈set (lcls (mbody m)). is_acc_type G (pid C) T;
jumpNestingOkS {Ret} (stmt (mbody m));
is_class G C;
⦇prg=G,cls=C,lcl=callee_lcl C sig m⦈⊢(stmt (mbody m))∷√;
(∃ A. ⦇prg=G,cls=C,lcl=callee_lcl C sig m⦈⊢ parameters m »⟨stmt (mbody m)⟩» A
∧ Result ∈ nrm A)
⟧ ⟹ P
⟧ ⟹ P"
by (unfold wf_mdecl_def) simp
lemma wf_mdeclD1:
"wf_mdecl G C (sig,m) ⟹
wf_mhead G (pid C) sig (mhead m) ∧ unique (lcls (mbody m)) ∧
(∀pn∈set (pars m). table_of (lcls (mbody m)) pn = None) ∧
(∀(vn,T)∈set (lcls (mbody m)). is_acc_type G (pid C) T)"
apply (unfold wf_mdecl_def)
apply simp
done
lemma wf_mdecl_bodyD:
"wf_mdecl G C (sig,m) ⟹
(∃T. ⦇prg=G,cls=C,lcl=callee_lcl C sig m⦈⊢Body C (stmt (mbody m))∷-T ∧
G⊢T≼(resTy m))"
apply (unfold wf_mdecl_def)
apply clarify
apply (rule_tac x="(resTy m)" in exI)
apply (unfold wf_mhead_def)
apply (auto simp add: wf_mhead_def is_acc_type_def intro: wt.Body )
done
lemma rT_is_acc_type:
"wf_mhead G P sig m ⟹ is_acc_type G P (resTy m)"
apply (unfold wf_mhead_def)
apply auto
done
subsubsection "well-formed interface declarations"
text ‹
A interface declaration is wellformed if:
\begin{itemize}
\item the interface hierarchy is wellstructured
\item there is no class with the same name
\item the method heads are wellformed and not static and have Public access
\item the methods are uniquely named
\item all superinterfaces are accessible
\item the result type of a method overriding a method of Object widens to the
result type of the overridden method.
Shadowing static methods is forbidden.
\item the result type of a method overriding a set of methods defined in the
superinterfaces widens to each of the corresponding result types
\end{itemize}
›
definition
wf_idecl :: "prog ⇒ idecl ⇒ bool" where
"wf_idecl G =
(λ(I,i).
ws_idecl G I (isuperIfs i) ∧
¬is_class G I ∧
(∀(sig,mh)∈set (imethods i). wf_mhead G (pid I) sig mh ∧
¬is_static mh ∧
accmodi mh = Public) ∧
unique (imethods i) ∧
(∀ J∈set (isuperIfs i). is_acc_iface G (pid I) J) ∧
(table_of (imethods i)
hiding (methd G Object)
under (λ new old. accmodi old ≠ Private)
entails (λnew old. G⊢resTy new≼resTy old ∧
is_static new = is_static old)) ∧
(set_option ∘ table_of (imethods i)
hidings Un_tables((λJ.(imethds G J))`set (isuperIfs i))
entails (λnew old. G⊢resTy new≼resTy old)))"
lemma wf_idecl_mhead: "⟦wf_idecl G (I,i); (sig,mh)∈set (imethods i)⟧ ⟹
wf_mhead G (pid I) sig mh ∧ ¬is_static mh ∧ accmodi mh = Public"
apply (unfold wf_idecl_def)
apply auto
done
lemma wf_idecl_hidings:
"wf_idecl G (I, i) ⟹
(λs. set_option (table_of (imethods i) s))
hidings Un_tables ((λJ. imethds G J) ` set (isuperIfs i))
entails λnew old. G⊢resTy new≼resTy old"
apply (unfold wf_idecl_def o_def)
apply simp
done
lemma wf_idecl_hiding:
"wf_idecl G (I, i) ⟹
(table_of (imethods i)
hiding (methd G Object)
under (λ new old. accmodi old ≠ Private)
entails (λnew old. G⊢resTy new≼resTy old ∧
is_static new = is_static old))"
apply (unfold wf_idecl_def)
apply simp
done
lemma wf_idecl_supD:
"⟦wf_idecl G (I,i); J ∈ set (isuperIfs i)⟧
⟹ is_acc_iface G (pid I) J ∧ (J, I) ∉ (subint1 G)⇧+"
apply (unfold wf_idecl_def ws_idecl_def)
apply auto
done
subsubsection "well-formed class declarations"
text ‹
A class declaration is wellformed if:
\begin{itemize}
\item there is no interface with the same name
\item all superinterfaces are accessible and for all methods implementing
an interface method the result type widens to the result type of
the interface method, the method is not static and offers at least
as much access
(this actually means that the method has Public access, since all
interface methods have public access)
\item all field declarations are wellformed and the field names are unique
\item all method declarations are wellformed and the method names are unique
\item the initialization statement is welltyped
\item the classhierarchy is wellstructured
\item Unless the class is Object:
\begin{itemize}
\item the superclass is accessible
\item for all methods overriding another method (of a superclass )the
result type widens to the result type of the overridden method,
the access modifier of the new method provides at least as much
access as the overwritten one.
\item for all methods hiding a method (of a superclass) the hidden
method must be static and offer at least as much access rights.
Remark: In contrast to the Java Language Specification we don't
restrict the result types of the method
(as in case of overriding), because there seems to be no reason,
since there is no dynamic binding of static methods.
(cf. 8.4.6.3 vs. 15.12.1).
Stricly speaking the restrictions on the access rights aren't
necessary to, since the static type and the access rights
together determine which method is to be called statically.
But if a class gains more then one static method with the
same signature due to inheritance, it is confusing when the
method selection depends on the access rights only:
e.g.
Class C declares static public method foo().
Class D is subclass of C and declares static method foo()
with default package access.
D.foo() ? if this call is in the same package as D then
foo of class D is called, otherwise foo of class C.
\end{itemize}
\end{itemize}
›
definition
entails :: "('a,'b) table ⇒ ('b ⇒ bool) ⇒ bool" ("_ entails _" 20)
where "(t entails P) = (∀k. ∀ x ∈ t k: P x)"
lemma entailsD:
"⟦t entails P; t k = Some x⟧ ⟹ P x"
by (simp add: entails_def)
lemma empty_entails[simp]: "Map.empty entails P"
by (simp add: entails_def)
definition
wf_cdecl :: "prog ⇒ cdecl ⇒ bool" where
"wf_cdecl G =
(λ(C,c).
¬is_iface G C ∧
(∀I∈set (superIfs c). is_acc_iface G (pid C) I ∧
(∀s. ∀ im ∈ imethds G I s.
(∃ cm ∈ methd G C s: G⊢resTy cm≼resTy im ∧
¬ is_static cm ∧
accmodi im ≤ accmodi cm))) ∧
(∀f∈set (cfields c). wf_fdecl G (pid C) f) ∧ unique (cfields c) ∧
(∀m∈set (methods c). wf_mdecl G C m) ∧ unique (methods c) ∧
jumpNestingOkS {} (init c) ∧
(∃ A. ⦇prg=G,cls=C,lcl=Map.empty⦈⊢ {} »⟨init c⟩» A) ∧
⦇prg=G,cls=C,lcl=Map.empty⦈⊢(init c)∷√ ∧ ws_cdecl G C (super c) ∧
(C ≠ Object ⟶
(is_acc_class G (pid C) (super c) ∧
(table_of (map (λ (s,m). (s,C,m)) (methods c))
entails (λ new. ∀ old sig.
(G,sig⊢new overrides⇩S old
⟶ (G⊢resTy new≼resTy old ∧
accmodi old ≤ accmodi new ∧
¬is_static old)) ∧
(G,sig⊢new hides old
⟶ (accmodi old ≤ accmodi new ∧
is_static old))))
)))"
lemma wf_cdeclE [consumes 1]:
"⟦wf_cdecl G (C,c);
⟦¬is_iface G C;
(∀I∈set (superIfs c). is_acc_iface G (pid C) I ∧
(∀s. ∀ im ∈ imethds G I s.
(∃ cm ∈ methd G C s: G⊢resTy cm≼resTy im ∧
¬ is_static cm ∧
accmodi im ≤ accmodi cm)));
∀f∈set (cfields c). wf_fdecl G (pid C) f; unique (cfields c);
∀m∈set (methods c). wf_mdecl G C m; unique (methods c);
jumpNestingOkS {} (init c);
∃ A. ⦇prg=G,cls=C,lcl=Map.empty⦈⊢ {} »⟨init c⟩» A;
⦇prg=G,cls=C,lcl=Map.empty⦈⊢(init c)∷√;
ws_cdecl G C (super c);
(C ≠ Object ⟶
(is_acc_class G (pid C) (super c) ∧
(table_of (map (λ (s,m). (s,C,m)) (methods c))
entails (λ new. ∀ old sig.
(G,sig⊢new overrides⇩S old
⟶ (G⊢resTy new≼resTy old ∧
accmodi old ≤ accmodi new ∧
¬is_static old)) ∧
(G,sig⊢new hides old
⟶ (accmodi old ≤ accmodi new ∧
is_static old))))
))⟧ ⟹ P
⟧ ⟹ P"
by (unfold wf_cdecl_def) simp
lemma wf_cdecl_unique:
"wf_cdecl G (C,c) ⟹ unique (cfields c) ∧ unique (methods c)"
apply (unfold wf_cdecl_def)
apply auto
done
lemma wf_cdecl_fdecl:
"⟦wf_cdecl G (C,c); f∈set (cfields c)⟧ ⟹ wf_fdecl G (pid C) f"
apply (unfold wf_cdecl_def)
apply auto
done
lemma wf_cdecl_mdecl:
"⟦wf_cdecl G (C,c); m∈set (methods c)⟧ ⟹ wf_mdecl G C m"
apply (unfold wf_cdecl_def)
apply auto
done
lemma wf_cdecl_impD:
"⟦wf_cdecl G (C,c); I∈set (superIfs c)⟧
⟹ is_acc_iface G (pid C) I ∧
(∀s. ∀im ∈ imethds G I s.
(∃cm ∈ methd G C s: G⊢resTy cm≼resTy im ∧ ¬is_static cm ∧
accmodi im ≤ accmodi cm))"
apply (unfold wf_cdecl_def)
apply auto
done
lemma wf_cdecl_supD:
"⟦wf_cdecl G (C,c); C ≠ Object⟧ ⟹
is_acc_class G (pid C) (super c) ∧ (super c,C) ∉ (subcls1 G)⇧+ ∧
(table_of (map (λ (s,m). (s,C,m)) (methods c))
entails (λ new. ∀ old sig.
(G,sig⊢new overrides⇩S old
⟶ (G⊢resTy new≼resTy old ∧
accmodi old ≤ accmodi new ∧
¬is_static old)) ∧
(G,sig⊢new hides old
⟶ (accmodi old ≤ accmodi new ∧
is_static old))))"
apply (unfold wf_cdecl_def ws_cdecl_def)
apply auto
done
lemma wf_cdecl_overrides_SomeD:
"⟦wf_cdecl G (C,c); C ≠ Object; table_of (methods c) sig = Some newM;
G,sig⊢(C,newM) overrides⇩S old
⟧ ⟹ G⊢resTy newM≼resTy old ∧
accmodi old ≤ accmodi newM ∧
¬ is_static old"
apply (drule (1) wf_cdecl_supD)
apply (clarify)
apply (drule entailsD)
apply (blast intro: table_of_map_SomeI)
apply (drule_tac x="old" in spec)
apply (auto dest: overrides_eq_sigD simp add: msig_def)
done
lemma wf_cdecl_hides_SomeD:
"⟦wf_cdecl G (C,c); C ≠ Object; table_of (methods c) sig = Some newM;
G,sig⊢(C,newM) hides old
⟧ ⟹ accmodi old ≤ access newM ∧
is_static old"
apply (drule (1) wf_cdecl_supD)
apply (clarify)
apply (drule entailsD)
apply (blast intro: table_of_map_SomeI)
apply (drule_tac x="old" in spec)
apply (auto dest: hides_eq_sigD simp add: msig_def)
done
lemma wf_cdecl_wt_init:
"wf_cdecl G (C, c) ⟹ ⦇prg=G,cls=C,lcl=Map.empty⦈⊢init c∷√"
apply (unfold wf_cdecl_def)
apply auto
done
subsubsection "well-formed programs"
text ‹
A program declaration is wellformed if:
\begin{itemize}
\item the class ObjectC of Object is defined
\item every method of Object has an access modifier distinct from Package.
This is
necessary since every interface automatically inherits from Object.
We must know, that every time a Object method is "overriden" by an
interface method this is also overriden by the class implementing the
the interface (see ‹implement_dynmethd and class_mheadsD›)
\item all standard Exceptions are defined
\item all defined interfaces are wellformed
\item all defined classes are wellformed
\end{itemize}
›
definition
wf_prog :: "prog ⇒ bool" where
"wf_prog G = (let is = ifaces G; cs = classes G in
ObjectC ∈ set cs ∧
(∀ m∈set Object_mdecls. accmodi m ≠ Package) ∧
(∀xn. SXcptC xn ∈ set cs) ∧
(∀i∈set is. wf_idecl G i) ∧ unique is ∧
(∀c∈set cs. wf_cdecl G c) ∧ unique cs)"
lemma wf_prog_idecl: "⟦iface G I = Some i; wf_prog G⟧ ⟹ wf_idecl G (I,i)"
apply (unfold wf_prog_def Let_def)
apply simp
apply (fast dest: map_of_SomeD)
done
lemma wf_prog_cdecl: "⟦class G C = Some c; wf_prog G⟧ ⟹ wf_cdecl G (C,c)"
apply (unfold wf_prog_def Let_def)
apply simp
apply (fast dest: map_of_SomeD)
done
lemma wf_prog_Object_mdecls:
"wf_prog G ⟹ (∀ m∈set Object_mdecls. accmodi m ≠ Package)"
apply (unfold wf_prog_def Let_def)
apply simp
done
lemma wf_prog_acc_superD:
"⟦wf_prog G; class G C = Some c; C ≠ Object ⟧
⟹ is_acc_class G (pid C) (super c)"
by (auto dest: wf_prog_cdecl wf_cdecl_supD)
lemma wf_ws_prog [elim!,simp]: "wf_prog G ⟹ ws_prog G"
apply (unfold wf_prog_def Let_def)
apply (rule ws_progI)
apply (simp_all (no_asm))
apply (auto simp add: is_acc_class_def is_acc_iface_def
dest!: wf_idecl_supD wf_cdecl_supD )+
done
lemma class_Object [simp]:
"wf_prog G ⟹
class G Object = Some ⦇access=Public,cfields=[],methods=Object_mdecls,
init=Skip,super=undefined,superIfs=[]⦈"
apply (unfold wf_prog_def Let_def ObjectC_def)
apply (fast dest!: map_of_SomeI)
done
lemma methd_Object[simp]: "wf_prog G ⟹ methd G Object =
table_of (map (λ(s,m). (s, Object, m)) Object_mdecls)"
apply (subst methd_rec)
apply (auto simp add: Let_def)
done
lemma wf_prog_Object_methd:
"⟦wf_prog G; methd G Object sig = Some m⟧ ⟹ accmodi m ≠ Package"
by (auto dest!: wf_prog_Object_mdecls) (auto dest!: map_of_SomeD)
lemma wf_prog_Object_is_public[intro]:
"wf_prog G ⟹ is_public G Object"
by (auto simp add: is_public_def dest: class_Object)
lemma class_SXcpt [simp]:
"wf_prog G ⟹
class G (SXcpt xn) = Some ⦇access=Public,cfields=[],methods=SXcpt_mdecls,
init=Skip,
super=if xn = Throwable then Object
else SXcpt Throwable,
superIfs=[]⦈"
apply (unfold wf_prog_def Let_def SXcptC_def)
apply (fast dest!: map_of_SomeI)
done
lemma wf_ObjectC [simp]:
"wf_cdecl G ObjectC = (¬is_iface G Object ∧ Ball (set Object_mdecls)
(wf_mdecl G Object) ∧ unique Object_mdecls)"
apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def)
apply (auto intro: da.Skip)
done
lemma Object_is_class [simp,elim!]: "wf_prog G ⟹ is_class G Object"
apply (simp (no_asm_simp))
done
lemma Object_is_acc_class [simp,elim!]: "wf_prog G ⟹ is_acc_class G S Object"
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
accessible_in_RefT_simp)
done
lemma SXcpt_is_class [simp,elim!]: "wf_prog G ⟹ is_class G (SXcpt xn)"
apply (simp (no_asm_simp))
done
lemma SXcpt_is_acc_class [simp,elim!]:
"wf_prog G ⟹ is_acc_class G S (SXcpt xn)"
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
accessible_in_RefT_simp)
done
lemma fields_Object [simp]: "wf_prog G ⟹ DeclConcepts.fields G Object = []"
by (force intro: fields_emptyI)
lemma accfield_Object [simp]:
"wf_prog G ⟹ accfield G S Object = Map.empty"
apply (unfold accfield_def)
apply (simp (no_asm_simp) add: Let_def)
done
lemma fields_Throwable [simp]:
"wf_prog G ⟹ DeclConcepts.fields G (SXcpt Throwable) = []"
by (force intro: fields_emptyI)
lemma fields_SXcpt [simp]: "wf_prog G ⟹ DeclConcepts.fields G (SXcpt xn) = []"
apply (case_tac "xn = Throwable")
apply (simp (no_asm_simp))
by (force intro: fields_emptyI)
lemmas widen_trans = ws_widen_trans [OF _ _ wf_ws_prog, elim]
lemma widen_trans2 [elim]: "⟦G⊢U≼T; G⊢S≼U; wf_prog G⟧ ⟹ G⊢S≼T"
apply (erule (2) widen_trans)
done
lemma Xcpt_subcls_Throwable [simp]:
"wf_prog G ⟹ G⊢SXcpt xn≼⇩C SXcpt Throwable"
apply (rule SXcpt_subcls_Throwable_lemma)
apply auto
done
lemma unique_fields:
"⟦is_class G C; wf_prog G⟧ ⟹ unique (DeclConcepts.fields G C)"
apply (erule ws_unique_fields)
apply (erule wf_ws_prog)
apply (erule (1) wf_prog_cdecl [THEN wf_cdecl_unique [THEN conjunct1]])
done
lemma fields_mono:
"⟦table_of (DeclConcepts.fields G C) fn = Some f; G⊢D≼⇩C C;
is_class G D; wf_prog G⟧
⟹ table_of (DeclConcepts.fields G D) fn = Some f"
apply (rule map_of_SomeI)
apply (erule (1) unique_fields)
apply (erule (1) map_of_SomeD [THEN fields_mono_lemma])
apply (erule wf_ws_prog)
done
lemma fields_is_type [elim]:
"⟦table_of (DeclConcepts.fields G C) m = Some f; wf_prog G; is_class G C⟧ ⟹
is_type G (type f)"
apply (frule wf_ws_prog)
apply (force dest: fields_declC [THEN conjunct1]
wf_prog_cdecl [THEN wf_cdecl_fdecl]
simp add: wf_fdecl_def2 is_acc_type_def)
done
lemma imethds_wf_mhead [rule_format (no_asm)]:
"⟦m ∈ imethds G I sig; wf_prog G; is_iface G I⟧ ⟹
wf_mhead G (pid (decliface m)) sig (mthd m) ∧
¬ is_static m ∧ accmodi m = Public"
apply (frule wf_ws_prog)
apply (drule (2) imethds_declI [THEN conjunct1])
apply clarify
apply (frule_tac I="(decliface m)" in wf_prog_idecl,assumption)
apply (drule wf_idecl_mhead)
apply (erule map_of_SomeD)
apply (cases m, simp)
done
lemma methd_wf_mdecl:
"⟦methd G C sig = Some m; wf_prog G; class G C = Some y⟧ ⟹
G⊢C≼⇩C (declclass m) ∧ is_class G (declclass m) ∧
wf_mdecl G (declclass m) (sig,(mthd m))"
apply (frule wf_ws_prog)
apply (drule (1) methd_declC)
apply fast
apply clarsimp
apply (frule (1) wf_prog_cdecl, erule wf_cdecl_mdecl, erule map_of_SomeD)
done
lemma methd_rT_is_type:
"⟦wf_prog G;methd G C sig = Some m;
class G C = Some y⟧
⟹ is_type G (resTy m)"
apply (drule (2) methd_wf_mdecl)
apply clarify
apply (drule wf_mdeclD1)
apply clarify
apply (drule rT_is_acc_type)
apply (cases m, simp add: is_acc_type_def)
done
lemma accmethd_rT_is_type:
"⟦wf_prog G;accmethd G S C sig = Some m;
class G C = Some y⟧
⟹ is_type G (resTy m)"
by (auto simp add: accmethd_def
intro: methd_rT_is_type)
lemma methd_Object_SomeD:
"⟦wf_prog G;methd G Object sig = Some m⟧
⟹ declclass m = Object"
by (auto dest: class_Object simp add: methd_rec )
lemmas iface_rec_induct' = iface_rec.induct [of "%x y z. P x y"] for P
lemma wf_imethdsD:
"⟦im ∈ imethds G I sig;wf_prog G; is_iface G I⟧
⟹ ¬is_static im ∧ accmodi im = Public"
proof -
assume asm: "wf_prog G" "is_iface G I" "im ∈ imethds G I sig"
have "wf_prog G ⟶
(∀ i im. iface G I = Some i ⟶ im ∈ imethds G I sig
⟶ ¬is_static im ∧ accmodi im = Public)" (is "?P G I")
proof (induct G I rule: iface_rec_induct', intro allI impI)
fix G I i im
assume hyp: "⋀ i J. iface G I = Some i ⟹ ws_prog G ⟹ J ∈ set (isuperIfs i)
⟹ ?P G J"
assume wf: "wf_prog G" and if_I: "iface G I = Some i" and
im: "im ∈ imethds G I sig"
show "¬is_static im ∧ accmodi im = Public"
proof -
let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
let ?new = "(set_option ∘ table_of (map (λ(s, mh). (s, I, mh)) (imethods i)))"
from if_I wf im have imethds:"im ∈ (?inherited ⊕⊕ ?new) sig"
by (simp add: imethds_rec)
from wf if_I have
wf_supI: "∀ J. J ∈ set (isuperIfs i) ⟶ (∃ j. iface G J = Some j)"
by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD)
from wf if_I have
"∀ im ∈ set (imethods i). ¬ is_static im ∧ accmodi im = Public"
by (auto dest!: wf_prog_idecl wf_idecl_mhead)
then have new_ok: "∀ im. table_of (imethods i) sig = Some im
⟶ ¬ is_static im ∧ accmodi im = Public"
by (auto dest!: table_of_Some_in_set)
show ?thesis
proof (cases "?new sig = {}")
case True
from True wf wf_supI if_I imethds hyp
show ?thesis by (auto simp del: split_paired_All)
next
case False
from False wf wf_supI if_I imethds new_ok hyp
show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD)
qed
qed
qed
with asm show ?thesis by (auto simp del: split_paired_All)
qed
lemma wf_prog_hidesD:
assumes hides: "G ⊢new hides old" and wf: "wf_prog G"
shows
"accmodi old ≤ accmodi new ∧
is_static old"
proof -
from hides
obtain c where
clsNew: "class G (declclass new) = Some c" and
neqObj: "declclass new ≠ Object"
by (auto dest: hidesD declared_in_classD)
with hides obtain newM oldM where
newM: "table_of (methods c) (msig new) = Some newM" and
new: "new = (declclass new,(msig new),newM)" and
old: "old = (declclass old,(msig old),oldM)" and
"msig new = msig old"
by (cases new,cases old)
(auto dest: hidesD
simp add: cdeclaredmethd_def declared_in_def)
with hides
have hides':
"G,(msig new)⊢(declclass new,newM) hides (declclass old,oldM)"
by auto
from clsNew wf
have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
note wf_cdecl_hides_SomeD [OF this neqObj newM hides']
with new old
show ?thesis
by (cases new, cases old) auto
qed
text ‹Compare this lemma about static
overriding \<^term>‹G ⊢new overrides⇩S old› with the definition of
dynamic overriding \<^term>‹G ⊢new overrides old›.
Conforming result types and restrictions on the access modifiers of the old
and the new method are not part of the predicate for static overriding. But
they are enshured in a wellfromed program. Dynamic overriding has
no restrictions on the access modifiers but enforces confrom result types
as precondition. But with some efford we can guarantee the access modifier
restriction for dynamic overriding, too. See lemma
‹wf_prog_dyn_override_prop›.
›
lemma wf_prog_stat_overridesD:
assumes stat_override: "G ⊢new overrides⇩S old" and wf: "wf_prog G"
shows
"G⊢resTy new≼resTy old ∧
accmodi old ≤ accmodi new ∧
¬ is_static old"
proof -
from stat_override
obtain c where
clsNew: "class G (declclass new) = Some c" and
neqObj: "declclass new ≠ Object"
by (auto dest: stat_overrides_commonD declared_in_classD)
with stat_override obtain newM oldM where
newM: "table_of (methods c) (msig new) = Some newM" and
new: "new = (declclass new,(msig new),newM)" and
old: "old = (declclass old,(msig old),oldM)" and
"msig new = msig old"
by (cases new,cases old)
(auto dest: stat_overrides_commonD
simp add: cdeclaredmethd_def declared_in_def)
with stat_override
have stat_override':
"G,(msig new)⊢(declclass new,newM) overrides⇩S (declclass old,oldM)"
by auto
from clsNew wf
have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override']
with new old
show ?thesis
by (cases new, cases old) auto
qed
lemma static_to_dynamic_overriding:
assumes stat_override: "G⊢new overrides⇩S old" and wf : "wf_prog G"
shows "G⊢new overrides old"
proof -
from stat_override
show ?thesis (is "?Overrides new old")
proof (induct)
case (Direct new old superNew)
then have stat_override:"G⊢new overrides⇩S old"
by (rule stat_overridesR.Direct)
from stat_override wf
have resTy_widen: "G⊢resTy new≼resTy old" and
not_static_old: "¬ is_static old"
by (auto dest: wf_prog_stat_overridesD)
have not_private_new: "accmodi new ≠ Private"
proof -
from stat_override
have "accmodi old ≠ Private"
by (rule no_Private_stat_override)
moreover
from stat_override wf
have "accmodi old ≤ accmodi new"
by (auto dest: wf_prog_stat_overridesD)
ultimately
show ?thesis
by (auto dest: acc_modi_bottom)
qed
with Direct resTy_widen not_static_old
show "?Overrides new old"
by (auto intro: overridesR.Direct stat_override_declclasses_relation)
next
case (Indirect new inter old)
then show "?Overrides new old"
by (blast intro: overridesR.Indirect)
qed
qed
lemma non_Package_instance_method_inheritance:
assumes old_inheritable: "G⊢Method old inheritable_in (pid C)" and
accmodi_old: "accmodi old ≠ Package" and
instance_method: "¬ is_static old" and
subcls: "G⊢C ≺⇩C declclass old" and
old_declared: "G⊢Method old declared_in (declclass old)" and
wf: "wf_prog G"
shows "G⊢Method old member_of C ∨
(∃ new. G⊢ new overrides⇩S old ∧ G⊢Method new member_of C)"
proof -
from wf have ws: "ws_prog G" by auto
from old_declared have iscls_declC_old: "is_class G (declclass old)"
by (auto simp add: declared_in_def cdeclaredmethd_def)
from subcls have iscls_C: "is_class G C"
by (blast dest: subcls_is_class)
from iscls_C ws old_inheritable subcls
show ?thesis (is "?P C old")
proof (induct rule: ws_class_induct')
case Object
assume "G⊢Object≺⇩C declclass old"
then show "?P Object old"
by blast
next
case (Subcls C c)
assume cls_C: "class G C = Some c" and
neq_C_Obj: "C ≠ Object" and
hyp: "⟦G ⊢Method old inheritable_in pid (super c);
G⊢super c≺⇩C declclass old⟧ ⟹ ?P (super c) old" and
inheritable: "G ⊢Method old inheritable_in pid C" and
subclsC: "G⊢C≺⇩C declclass old"
from cls_C neq_C_Obj
have super: "G⊢C ≺⇩C1 super c"
by (rule subcls1I)
from wf cls_C neq_C_Obj
have accessible_super: "G⊢(Class (super c)) accessible_in (pid C)"
by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
{
fix old
assume member_super: "G⊢Method old member_of (super c)"
assume inheritable: "G ⊢Method old inheritable_in pid C"
assume instance_method: "¬ is_static old"
from member_super
have old_declared: "G⊢Method old declared_in (declclass old)"
by (cases old) (auto dest: member_of_declC)
have "?P C old"
proof (cases "G⊢mid (msig old) undeclared_in C")
case True
with inheritable super accessible_super member_super
have "G⊢Method old member_of C"
by (cases old) (auto intro: members.Inherited)
then show ?thesis
by auto
next
case False
then obtain new_member where
"G⊢new_member declared_in C" and
"mid (msig old) = memberid new_member"
by (auto dest: not_undeclared_declared)
then obtain new where
new: "G⊢Method new declared_in C" and
eq_sig: "msig old = msig new" and
declC_new: "declclass new = C"
by (cases new_member) auto
then have member_new: "G⊢Method new member_of C"
by (cases new) (auto intro: members.Immediate)
from declC_new super member_super
have subcls_new_old: "G⊢declclass new ≺⇩C declclass old"
by (auto dest!: member_of_subclseq_declC
dest: r_into_trancl intro: trancl_rtrancl_trancl)
show ?thesis
proof (cases "is_static new")
case False
with eq_sig declC_new new old_declared inheritable
super member_super subcls_new_old
have "G⊢new overrides⇩S old"
by (auto intro!: stat_overridesR.Direct)
with member_new show ?thesis
by blast
next
case True
with eq_sig declC_new subcls_new_old new old_declared inheritable
have "G⊢new hides old"
by (auto intro: hidesI)
with wf
have "is_static old"
by (blast dest: wf_prog_hidesD)
with instance_method
show ?thesis
by (contradiction)
qed
qed
} note hyp_member_super = this
from subclsC cls_C
have "G⊢(super c)≼⇩C declclass old"
by (rule subcls_superD)
then
show "?P C old"
proof (cases rule: subclseq_cases)
case Eq
assume "super c = declclass old"
with old_declared
have "G⊢Method old member_of (super c)"
by (cases old) (auto intro: members.Immediate)
with inheritable instance_method
show ?thesis
by (blast dest: hyp_member_super)
next
case Subcls
assume "G⊢super c≺⇩C declclass old"
moreover
from inheritable accmodi_old
have "G ⊢Method old inheritable_in pid (super c)"
by (cases "accmodi old") (auto simp add: inheritable_in_def)
ultimately
have "?P (super c) old"
by (blast dest: hyp)
then show ?thesis
proof
assume "G ⊢Method old member_of super c"
with inheritable instance_method
show ?thesis
by (blast dest: hyp_member_super)
next
assume "∃new. G ⊢ new overrides⇩S old ∧ G ⊢Method new member_of super c"
then obtain super_new where
super_new_override: "G ⊢ super_new overrides⇩S old" and
super_new_member: "G ⊢Method super_new member_of super c"
by blast
from super_new_override wf
have "accmodi old ≤ accmodi super_new"
by (auto dest: wf_prog_stat_overridesD)
with inheritable accmodi_old
have "G ⊢Method super_new inheritable_in pid C"
by (auto simp add: inheritable_in_def
split: acc_modi.splits
dest: acc_modi_le_Dests)
moreover
from super_new_override
have "¬ is_static super_new"
by (auto dest: stat_overrides_commonD)
moreover
note super_new_member
ultimately have "?P C super_new"
by (auto dest: hyp_member_super)
then show ?thesis
proof
assume "G ⊢Method super_new member_of C"
with super_new_override
show ?thesis
by blast
next
assume "∃new. G ⊢ new overrides⇩S super_new ∧
G ⊢Method new member_of C"
with super_new_override show ?thesis
by (blast intro: stat_overridesR.Indirect)
qed
qed
qed
qed
qed
lemma non_Package_instance_method_inheritance_cases:
assumes old_inheritable: "G⊢Method old inheritable_in (pid C)" and
accmodi_old: "accmodi old ≠ Package" and
instance_method: "¬ is_static old" and
subcls: "G⊢C ≺⇩C declclass old" and
old_declared: "G⊢Method old declared_in (declclass old)" and
wf: "wf_prog G"
obtains (Inheritance) "G⊢Method old member_of C"
| (Overriding) new where "G⊢ new overrides⇩S old" and "G⊢Method new member_of C"
proof -
from old_inheritable accmodi_old instance_method subcls old_declared wf
Inheritance Overriding
show thesis
by (auto dest: non_Package_instance_method_inheritance)
qed
lemma dynamic_to_static_overriding:
assumes dyn_override: "G⊢ new overrides old" and
accmodi_old: "accmodi old ≠ Package" and
wf: "wf_prog G"
shows "G⊢ new overrides⇩S old"
proof -
from dyn_override accmodi_old
show ?thesis (is "?Overrides new old")
proof (induct rule: overridesR.induct)
case (Direct new old)
assume new_declared: "G⊢Method new declared_in declclass new"
assume eq_sig_new_old: "msig new = msig old"
assume subcls_new_old: "G⊢declclass new ≺⇩C declclass old"
assume "G ⊢Method old inheritable_in pid (declclass new)" and
"accmodi old ≠ Package" and
"¬ is_static old" and
"G⊢declclass new≺⇩C declclass old" and
"G⊢Method old declared_in declclass old"
from this wf
show "?Overrides new old"
proof (cases rule: non_Package_instance_method_inheritance_cases)
case Inheritance
assume "G ⊢Method old member_of declclass new"
then have "G⊢mid (msig old) undeclared_in declclass new"
proof cases
case Immediate
with subcls_new_old wf show ?thesis
by (auto dest: subcls_irrefl)
next
case Inherited
then show ?thesis
by (cases old) auto
qed
with eq_sig_new_old new_declared
show ?thesis
by (cases old,cases new) (auto dest!: declared_not_undeclared)
next
case (Overriding new')
assume stat_override_new': "G ⊢ new' overrides⇩S old"
then have "msig new' = msig old"
by (auto dest: stat_overrides_commonD)
with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'"
by simp
assume "G ⊢Method new' member_of declclass new"
then show ?thesis
proof (cases)
case Immediate
then have declC_new: "declclass new' = declclass new"
by auto
from Immediate
have "G⊢Method new' declared_in declclass new"
by (cases new') auto
with new_declared eq_sig_new_new' declC_new
have "new=new'"
by (cases new, cases new') (auto dest: unique_declared_in)
with stat_override_new'
show ?thesis
by simp
next
case Inherited
then have "G⊢mid (msig new') undeclared_in declclass new"
by (cases new') (auto)
with eq_sig_new_new' new_declared
show ?thesis
by (cases new,cases new') (auto dest!: declared_not_undeclared)
qed
qed
next
case (Indirect new inter old)
assume accmodi_old: "accmodi old ≠ Package"
assume "accmodi old ≠ Package ⟹ G ⊢ inter overrides⇩S old"
with accmodi_old
have stat_override_inter_old: "G ⊢ inter overrides⇩S old"
by blast
moreover
assume hyp_inter: "accmodi inter ≠ Package ⟹ G ⊢ new overrides⇩S inter"
moreover
have "accmodi inter ≠ Package"
proof -
from stat_override_inter_old wf
have "accmodi old ≤ accmodi inter"
by (auto dest: wf_prog_stat_overridesD)
with stat_override_inter_old accmodi_old
show ?thesis
by (auto dest!: no_Private_stat_override
split: acc_modi.splits
dest: acc_modi_le_Dests)
qed
ultimately show "?Overrides new old"
by (blast intro: stat_overridesR.Indirect)
qed
qed
lemma wf_prog_dyn_override_prop:
assumes dyn_override: "G ⊢ new overrides old" and
wf: "wf_prog G"
shows "accmodi old ≤ accmodi new"
proof (cases "accmodi old = Package")
case True
note old_Package = this
show ?thesis
proof (cases "accmodi old ≤ accmodi new")
case True then show ?thesis .
next
case False
with old_Package
have "accmodi new = Private"
by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def)
with dyn_override
show ?thesis
by (auto dest: overrides_commonD)
qed
next
case False
with dyn_override wf
have "G ⊢ new overrides⇩S old"
by (blast intro: dynamic_to_static_overriding)
with wf
show ?thesis
by (blast dest: wf_prog_stat_overridesD)
qed
lemma overrides_Package_old:
assumes dyn_override: "G ⊢ new overrides old" and
accmodi_new: "accmodi new = Package" and
wf: "wf_prog G "
shows "accmodi old = Package"
proof (cases "accmodi old")
case Private
with dyn_override show ?thesis
by (simp add: no_Private_override)
next
case Package
then show ?thesis .
next
case Protected
with dyn_override wf
have "G ⊢ new overrides⇩S old"
by (auto intro: dynamic_to_static_overriding)
with wf
have "accmodi old ≤ accmodi new"
by (auto dest: wf_prog_stat_overridesD)
with Protected accmodi_new
show ?thesis
by (simp add: less_acc_def le_acc_def)
next
case Public
with dyn_override wf
have "G ⊢ new overrides⇩S old"
by (auto intro: dynamic_to_static_overriding)
with wf
have "accmodi old ≤ accmodi new"
by (auto dest: wf_prog_stat_overridesD)
with Public accmodi_new
show ?thesis
by (simp add: less_acc_def le_acc_def)
qed
lemma dyn_override_Package:
assumes dyn_override: "G ⊢ new overrides old" and
accmodi_old: "accmodi old = Package" and
accmodi_new: "accmodi new = Package" and
wf: "wf_prog G"
shows "pid (declclass old) = pid (declclass new)"
proof -
from dyn_override accmodi_old accmodi_new
show ?thesis (is "?EqPid old new")
proof (induct rule: overridesR.induct)
case (Direct new old)
assume "accmodi old = Package"
"G ⊢Method old inheritable_in pid (declclass new)"
then show "pid (declclass old) = pid (declclass new)"
by (auto simp add: inheritable_in_def)
next
case (Indirect new inter old)
assume accmodi_old: "accmodi old = Package" and
accmodi_new: "accmodi new = Package"
assume "G ⊢ new overrides inter"
with accmodi_new wf
have "accmodi inter = Package"
by (auto intro: overrides_Package_old)
with Indirect
show "pid (declclass old) = pid (declclass new)"
by auto
qed
qed
lemma dyn_override_Package_escape:
assumes dyn_override: "G ⊢ new overrides old" and
accmodi_old: "accmodi old = Package" and
outside_pack: "pid (declclass old) ≠ pid (declclass new)" and
wf: "wf_prog G"
shows "∃ inter. G ⊢ new overrides inter ∧ G ⊢ inter overrides old ∧
pid (declclass old) = pid (declclass inter) ∧
Protected ≤ accmodi inter"
proof -
from dyn_override accmodi_old outside_pack
show ?thesis (is "?P new old")
proof (induct rule: overridesR.induct)
case (Direct new old)
assume accmodi_old: "accmodi old = Package"
assume outside_pack: "pid (declclass old) ≠ pid (declclass new)"
assume "G ⊢Method old inheritable_in pid (declclass new)"
with accmodi_old
have "pid (declclass old) = pid (declclass new)"
by (simp add: inheritable_in_def)
with outside_pack
show "?P new old"
by (contradiction)
next
case (Indirect new inter old)
assume accmodi_old: "accmodi old = Package"
assume outside_pack: "pid (declclass old) ≠ pid (declclass new)"
assume override_new_inter: "G ⊢ new overrides inter"
assume override_inter_old: "G ⊢ inter overrides old"
assume hyp_new_inter: "⟦accmodi inter = Package;
pid (declclass inter) ≠ pid (declclass new)⟧
⟹ ?P new inter"
assume hyp_inter_old: "⟦accmodi old = Package;
pid (declclass old) ≠ pid (declclass inter)⟧
⟹ ?P inter old"
show "?P new old"
proof (cases "pid (declclass old) = pid (declclass inter)")
case True
note same_pack_old_inter = this
show ?thesis
proof (cases "pid (declclass inter) = pid (declclass new)")
case True
with same_pack_old_inter outside_pack
show ?thesis
by auto
next
case False
note diff_pack_inter_new = this
show ?thesis
proof (cases "accmodi inter = Package")
case True
with diff_pack_inter_new hyp_new_inter
obtain newinter where
over_new_newinter: "G ⊢ new overrides newinter" and
over_newinter_inter: "G ⊢ newinter overrides inter" and
eq_pid: "pid (declclass inter) = pid (declclass newinter)" and
accmodi_newinter: "Protected ≤ accmodi newinter"
by auto
from over_newinter_inter override_inter_old
have "G⊢newinter overrides old"
by (rule overridesR.Indirect)
moreover
from eq_pid same_pack_old_inter
have "pid (declclass old) = pid (declclass newinter)"
by simp
moreover
note over_new_newinter accmodi_newinter
ultimately show ?thesis
by blast
next
case False
with override_new_inter
have "Protected ≤ accmodi inter"
by (cases "accmodi inter") (auto dest: no_Private_override)
with override_new_inter override_inter_old same_pack_old_inter
show ?thesis
by blast
qed
qed
next
case False
with accmodi_old hyp_inter_old
obtain newinter where
over_inter_newinter: "G ⊢ inter overrides newinter" and
over_newinter_old: "G ⊢ newinter overrides old" and
eq_pid: "pid (declclass old) = pid (declclass newinter)" and
accmodi_newinter: "Protected ≤ accmodi newinter"
by auto
from override_new_inter over_inter_newinter
have "G ⊢ new overrides newinter"
by (rule overridesR.Indirect)
with eq_pid over_newinter_old accmodi_newinter
show ?thesis
by blast
qed
qed
qed
lemmas class_rec_induct' = class_rec.induct [of "%x y z w. P x y"] for P
lemma declclass_widen[rule_format]:
"wf_prog G
⟶ (∀c m. class G C = Some c ⟶ methd G C sig = Some m
⟶ G⊢C ≼⇩C declclass m)" (is "?P G C")
proof (induct G C rule: class_rec_induct', intro allI impI)
fix G C c m
assume Hyp: "⋀c. class G C = Some c ⟹ ws_prog G ⟹ C ≠ Object
⟹ ?P G (super c)"
assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
m: "methd G C sig = Some m"
show "G⊢C≼⇩C declclass m"
proof (cases "C=Object")
case True
with wf m show ?thesis by (simp add: methd_Object_SomeD)
next
let ?filter="filter_tab (λsig m. G⊢C inherits method sig m)"
let ?table = "table_of (map (λ(s, m). (s, C, m)) (methods c))"
case False
with cls_C wf m
have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
by (simp add: methd_rec)
show ?thesis
proof (cases "?table sig")
case None
from this methd_C have "?filter (methd G (super c)) sig = Some m"
by simp
moreover
from wf cls_C False obtain sup where "class G (super c) = Some sup"
by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
moreover note wf False cls_C
ultimately have "G⊢super c ≼⇩C declclass m"
by (auto intro: Hyp [rule_format])
moreover from cls_C False have "G⊢C ≺⇩C1 super c" by (rule subcls1I)
ultimately show ?thesis by - (rule rtrancl_into_rtrancl2)
next
case Some
from this wf False cls_C methd_C show ?thesis by auto
qed
qed
qed
lemma declclass_methd_Object:
"⟦wf_prog G; methd G Object sig = Some m⟧ ⟹ declclass m = Object"
by auto
lemma methd_declaredD:
"⟦wf_prog G; is_class G C;methd G C sig = Some m⟧
⟹ G⊢(mdecl (sig,mthd m)) declared_in (declclass m)"
proof -
assume wf: "wf_prog G"
then have ws: "ws_prog G" ..
assume clsC: "is_class G C"
from clsC ws
show "methd G C sig = Some m
⟹ G⊢(mdecl (sig,mthd m)) declared_in (declclass m)"
proof (induct C rule: ws_class_induct')
case Object
assume "methd G Object sig = Some m"
with wf show ?thesis
by - (rule method_declared_inI, auto)
next
case Subcls
fix C c
assume clsC: "class G C = Some c"
and m: "methd G C sig = Some m"
and hyp: "methd G (super c) sig = Some m ⟹ ?thesis"
let ?newMethods = "table_of (map (λ(s, m). (s, C, m)) (methods c))"
show ?thesis
proof (cases "?newMethods sig")
case None
from None ws clsC m hyp
show ?thesis by (auto intro: method_declared_inI simp add: methd_rec)
next
case Some
from Some ws clsC m
show ?thesis by (auto intro: method_declared_inI simp add: methd_rec)
qed
qed
qed
lemma methd_rec_Some_cases:
assumes methd_C: "methd G C sig = Some m" and
ws: "ws_prog G" and
clsC: "class G C = Some c" and
neq_C_Obj: "C≠Object"
obtains (NewMethod) "table_of (map (λ(s, m). (s, C, m)) (methods c)) sig = Some m"
| (InheritedMethod) "G⊢C inherits (method sig m)" and "methd G (super c) sig = Some m"
proof -
let ?inherited = "filter_tab (λsig m. G⊢C inherits method sig m)
(methd G (super c))"
let ?new = "table_of (map (λ(s, m). (s, C, m)) (methods c))"
from ws clsC neq_C_Obj methd_C
have methd_unfold: "(?inherited ++ ?new) sig = Some m"
by (simp add: methd_rec)
show thesis
proof (cases "?new sig")
case None
with methd_unfold have "?inherited sig = Some m"
by (auto)
with InheritedMethod show ?thesis by blast
next
case Some
with methd_unfold have "?new sig = Some m"
by auto
with NewMethod show ?thesis by blast
qed
qed
lemma methd_member_of:
assumes wf: "wf_prog G"
shows
"⟦is_class G C; methd G C sig = Some m⟧ ⟹ G⊢Methd sig m member_of C"
(is "?Class C ⟹ ?Method C ⟹ ?MemberOf C")
proof -
from wf have ws: "ws_prog G" ..
assume defC: "is_class G C"
from defC ws
show "?Class C ⟹ ?Method C ⟹ ?MemberOf C"
proof (induct rule: ws_class_induct')
case Object
with wf have declC: "Object = declclass m"
by (simp add: declclass_methd_Object)
from Object wf have "G⊢Methd sig m declared_in Object"
by (auto intro: methd_declaredD simp add: declC)
with declC
show "?MemberOf Object"
by (auto intro!: members.Immediate
simp del: methd_Object)
next
case (Subcls C c)
assume clsC: "class G C = Some c" and
neq_C_Obj: "C ≠ Object"
assume methd: "?Method C"
from methd ws clsC neq_C_Obj
show "?MemberOf C"
proof (cases rule: methd_rec_Some_cases)
case NewMethod
with clsC show ?thesis
by (auto dest: method_declared_inI intro!: members.Immediate)
next
case InheritedMethod
then show "?thesis"
by (blast dest: inherits_member)
qed
qed
qed
lemma current_methd:
"⟦table_of (methods c) sig = Some new;
ws_prog G; class G C = Some c; C ≠ Object;
methd G (super c) sig = Some old⟧
⟹ methd G C sig = Some (C,new)"
by (auto simp add: methd_rec
intro: filter_tab_SomeI map_add_find_right table_of_map_SomeI)
lemma wf_prog_staticD:
assumes wf: "wf_prog G" and
clsC: "class G C = Some c" and
neq_C_Obj: "C ≠ Object" and
old: "methd G (super c) sig = Some old" and
accmodi_old: "Protected ≤ accmodi old" and
new: "table_of (methods c) sig = Some new"
shows "is_static new = is_static old"
proof -
from clsC wf
have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl)
from wf clsC neq_C_Obj
have is_cls_super: "is_class G (super c)"
by (blast dest: wf_prog_acc_superD is_acc_classD)
from wf is_cls_super old
have old_member_of: "G⊢Methd sig old member_of (super c)"
by (rule methd_member_of)
from old wf is_cls_super
have old_declared: "G⊢Methd sig old declared_in (declclass old)"
by (auto dest: methd_declared_in_declclass)
from new clsC
have new_declared: "G⊢Methd sig (C,new) declared_in C"
by (auto intro: method_declared_inI)
note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans]
from clsC neq_C_Obj
have subcls1_C_super: "G⊢C ≺⇩C1 super c"
by (rule subcls1I)
then have "G⊢C ≺⇩C super c" ..
also from old wf is_cls_super
have "G⊢super c ≼⇩C (declclass old)" by (auto dest: methd_declC)
finally have subcls_C_old: "G⊢C ≺⇩C (declclass old)" .
from accmodi_old
have inheritable: "G⊢Methd sig old inheritable_in pid C"
by (auto simp add: inheritable_in_def
dest: acc_modi_le_Dests)
show ?thesis
proof (cases "is_static new")
case True
with subcls_C_old new_declared old_declared inheritable
have "G,sig⊢(C,new) hides old"
by (auto intro: hidesI)
with True wf_cdecl neq_C_Obj new
show ?thesis
by (auto dest: wf_cdecl_hides_SomeD)
next
case False
with subcls_C_old new_declared old_declared inheritable subcls1_C_super
old_member_of
have "G,sig⊢(C,new) overrides⇩S old"
by (auto intro: stat_overridesR.Direct)
with False wf_cdecl neq_C_Obj new
show ?thesis
by (auto dest: wf_cdecl_overrides_SomeD)
qed
qed
lemma inheritable_instance_methd:
assumes subclseq_C_D: "G⊢C ≼⇩C D" and
is_cls_D: "is_class G D" and
wf: "wf_prog G" and
old: "methd G D sig = Some old" and
accmodi_old: "Protected ≤ accmodi old" and
not_static_old: "¬ is_static old"
shows
"∃new. methd G C sig = Some new ∧
(new = old ∨ G,sig⊢new overrides⇩S old)"
(is "(∃new. (?Constraint C new old))")
proof -
from subclseq_C_D is_cls_D
have is_cls_C: "is_class G C" by (rule subcls_is_class2)
from wf
have ws: "ws_prog G" ..
from is_cls_C ws subclseq_C_D
show "∃new. ?Constraint C new old"
proof (induct rule: ws_class_induct')
case (Object co)
then have eq_D_Obj: "D=Object" by auto
with old
have "?Constraint Object old old"
by auto
with eq_D_Obj
show "∃ new. ?Constraint Object new old" by auto
next
case (Subcls C c)
assume hyp: "G⊢super c≼⇩C D ⟹ ∃new. ?Constraint (super c) new old"
assume clsC: "class G C = Some c"
assume neq_C_Obj: "C≠Object"
from clsC wf
have wf_cdecl: "wf_cdecl G (C,c)"
by (rule wf_prog_cdecl)
from ws clsC neq_C_Obj
have is_cls_super: "is_class G (super c)"
by (auto dest: ws_prog_cdeclD)
from clsC wf neq_C_Obj
have superAccessible: "G⊢(Class (super c)) accessible_in (pid C)" and
subcls1_C_super: "G⊢C ≺⇩C1 super c"
by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD
intro: subcls1I)
show "∃new. ?Constraint C new old"
proof (cases "G⊢super c≼⇩C D")
case False
from False Subcls
have eq_C_D: "C=D"
by (auto dest: subclseq_superD)
with old
have "?Constraint C old old"
by auto
with eq_C_D
show "∃ new. ?Constraint C new old" by auto
next
case True
with hyp obtain super_method
where super: "?Constraint (super c) super_method old" by blast
from super not_static_old
have not_static_super: "¬ is_static super_method"
by (auto dest!: stat_overrides_commonD)
from super old wf accmodi_old
have accmodi_super_method: "Protected ≤ accmodi super_method"
by (auto dest!: wf_prog_stat_overridesD)
from super accmodi_old wf
have inheritable: "G⊢Methd sig super_method inheritable_in (pid C)"
by (auto dest!: wf_prog_stat_overridesD
acc_modi_le_Dests
simp add: inheritable_in_def)
from super wf is_cls_super
have member: "G⊢Methd sig super_method member_of (super c)"
by (auto intro: methd_member_of)
from member
have decl_super_method:
"G⊢Methd sig super_method declared_in (declclass super_method)"
by (auto dest: member_of_declC)
from super subcls1_C_super ws is_cls_super
have subcls_C_super: "G⊢C ≺⇩C (declclass super_method)"
by (auto intro: rtrancl_into_trancl2 dest: methd_declC)
show "∃ new. ?Constraint C new old"
proof (cases "methd G C sig")
case None
have "methd G (super c) sig = None"
proof -
from clsC ws None
have no_new: "table_of (methods c) sig = None"
by (auto simp add: methd_rec)
with clsC
have undeclared: "G⊢mid sig undeclared_in C"
by (auto simp add: undeclared_in_def cdeclaredmethd_def)
with inheritable member superAccessible subcls1_C_super
have inherits: "G⊢C inherits (method sig super_method)"
by (auto simp add: inherits_def)
with clsC ws no_new super neq_C_Obj
have "methd G C sig = Some super_method"
by (auto simp add: methd_rec map_add_def intro: filter_tab_SomeI)
with None show ?thesis
by simp
qed
with super show ?thesis by auto
next
case (Some new)
from this ws clsC neq_C_Obj
show ?thesis
proof (cases rule: methd_rec_Some_cases)
case InheritedMethod
with super Some show ?thesis
by auto
next
case NewMethod
assume new: "table_of (map (λ(s, m). (s, C, m)) (methods c)) sig
= Some new"
from new
have declcls_new: "declclass new = C"
by auto
from wf clsC neq_C_Obj super new not_static_super accmodi_super_method
have not_static_new: "¬ is_static new"
by (auto dest: wf_prog_staticD)
from clsC new
have decl_new: "G⊢Methd sig new declared_in C"
by (auto simp add: declared_in_def cdeclaredmethd_def)
from not_static_new decl_new decl_super_method
member subcls1_C_super inheritable declcls_new subcls_C_super
have "G,sig⊢ new overrides⇩S super_method"
by (auto intro: stat_overridesR.Direct)
with super Some
show ?thesis
by (auto intro: stat_overridesR.Indirect)
qed
qed
qed
qed
qed
lemma inheritable_instance_methd_cases:
assumes subclseq_C_D: "G⊢C ≼⇩C D" and
is_cls_D: "is_class G D" and
wf: "wf_prog G" and
old: "methd G D sig = Some old" and
accmodi_old: "Protected ≤ accmodi old" and
not_static_old: "¬ is_static old"
obtains (Inheritance) "methd G C sig = Some old"
| (Overriding) new where "methd G C sig = Some new" and "G,sig⊢new overrides⇩S old"
proof -
from subclseq_C_D is_cls_D wf old accmodi_old not_static_old
show ?thesis
by (auto dest: inheritable_instance_methd intro: Inheritance Overriding)
qed
lemma inheritable_instance_methd_props:
assumes subclseq_C_D: "G⊢C ≼⇩C D" and
is_cls_D: "is_class G D" and
wf: "wf_prog G" and
old: "methd G D sig = Some old" and
accmodi_old: "Protected ≤ accmodi old" and
not_static_old: "¬ is_static old"
shows
"∃new. methd G C sig = Some new ∧
¬ is_static new ∧ G⊢resTy new≼resTy old ∧ accmodi old ≤accmodi new"
(is "(∃new. (?Constraint C new old))")
proof -
from subclseq_C_D is_cls_D wf old accmodi_old not_static_old
show ?thesis
proof (cases rule: inheritable_instance_methd_cases)
case Inheritance
with not_static_old accmodi_old show ?thesis by auto
next
case (Overriding new)
then have "¬ is_static new" by (auto dest: stat_overrides_commonD)
with Overriding not_static_old accmodi_old wf
show ?thesis
by (auto dest!: wf_prog_stat_overridesD)
qed
qed
lemma bexI': "x ∈ A ⟹ P x ⟹ ∃x∈A. P x" by blast
lemma ballE': "∀x∈A. P x ⟹ (x ∉ A ⟹ Q) ⟹ (P x ⟹ Q) ⟹ Q" by blast
lemma subint_widen_imethds:
assumes irel: "G⊢I≼I J"
and wf: "wf_prog G"
and is_iface: "is_iface G J"
and jm: "jm ∈ imethds G J sig"
shows "∃im ∈ imethds G I sig. is_static im = is_static jm ∧
accmodi im = accmodi jm ∧
G⊢resTy im≼resTy jm"
using irel jm
proof (induct rule: converse_rtrancl_induct)
case base
then show ?case by (blast elim: bexI')
next
case (step I SI)
from ‹G⊢I ≺I1 SI›
obtain i where
ifI: "iface G I = Some i" and
SI: "SI ∈ set (isuperIfs i)"
by (blast dest: subint1D)
let ?newMethods
= "(set_option ∘ table_of (map (λ(sig, mh). (sig, I, mh)) (imethods i)))"
show ?case
proof (cases "?newMethods sig = {}")
case True
with ifI SI step wf
show "?thesis"
by (auto simp add: imethds_rec)
next
case False
from ifI wf False
have imethds: "imethds G I sig = ?newMethods sig"
by (simp add: imethds_rec)
from False
obtain im where
imdef: "im ∈ ?newMethods sig"
by (blast)
with imethds
have im: "im ∈ imethds G I sig"
by (blast)
with im wf ifI
obtain
imStatic: "¬ is_static im" and
imPublic: "accmodi im = Public"
by (auto dest!: imethds_wf_mhead)
from ifI wf
have wf_I: "wf_idecl G (I,i)"
by (rule wf_prog_idecl)
with SI wf
obtain si where
ifSI: "iface G SI = Some si" and
wf_SI: "wf_idecl G (SI,si)"
by (auto dest!: wf_idecl_supD is_acc_ifaceD
dest: wf_prog_idecl)
from step
obtain sim::"qtname × mhead" where
sim: "sim ∈ imethds G SI sig" and
eq_static_sim_jm: "is_static sim = is_static jm" and
eq_access_sim_jm: "accmodi sim = accmodi jm" and
resTy_widen_sim_jm: "G⊢resTy sim≼resTy jm"
by blast
with wf_I SI imdef sim
have "G⊢resTy im≼resTy sim"
by (auto dest!: wf_idecl_hidings hidings_entailsD)
with wf resTy_widen_sim_jm
have resTy_widen_im_jm: "G⊢resTy im≼resTy jm"
by (blast intro: widen_trans)
from sim wf ifSI
obtain
simStatic: "¬ is_static sim" and
simPublic: "accmodi sim = Public"
by (auto dest!: imethds_wf_mhead)
from im
imStatic simStatic eq_static_sim_jm
imPublic simPublic eq_access_sim_jm
resTy_widen_im_jm
show ?thesis
by auto
qed
qed
lemma implmt1_methd:
"⋀sig. ⟦G⊢C↝1I; wf_prog G; im ∈ imethds G I sig⟧ ⟹
∃cm ∈methd G C sig: ¬ is_static cm ∧ ¬ is_static im ∧
G⊢resTy cm≼resTy im ∧
accmodi im = Public ∧ accmodi cm = Public"
apply (drule implmt1D)
apply clarify
apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_impD])
apply (frule (1) imethds_wf_mhead)
apply (simp add: is_acc_iface_def)
apply (force)
done
lemma implmt_methd [rule_format (no_asm)]:
"⟦wf_prog G; G⊢C↝I⟧ ⟹ is_iface G I ⟶
(∀ im ∈imethds G I sig.
∃ cm∈methd G C sig: ¬is_static cm ∧ ¬ is_static im ∧
G⊢resTy cm≼resTy im ∧
accmodi im = Public ∧ accmodi cm = Public)"
apply (frule implmt_is_class)
apply (erule implmt.induct)
apply safe
apply (drule (2) implmt1_methd)
apply fast
apply (drule (1) subint_widen_imethds)
apply simp
apply assumption
apply clarify
apply (drule (2) implmt1_methd)
apply (force)
apply (frule subcls1D)
apply (drule (1) bspec)
apply clarify
apply (drule (3) r_into_rtrancl [THEN inheritable_instance_methd_props,
OF _ implmt_is_class])
apply auto
done
lemma mheadsD [rule_format (no_asm)]:
"emh ∈ mheads G S t sig ⟶ wf_prog G ⟶
(∃C D m. t = ClassT C ∧ declrefT emh = ClassT D ∧
accmethd G S C sig = Some m ∧
(declclass m = D) ∧ mhead (mthd m) = (mhd emh)) ∨
(∃I. t = IfaceT I ∧ ((∃im. im ∈ accimethds G (pid S) I sig ∧
mthd im = mhd emh) ∨
(∃m. G⊢Iface I accessible_in (pid S) ∧ accmethd G S Object sig = Some m ∧
accmodi m ≠ Private ∧
declrefT emh = ClassT Object ∧ mhead (mthd m) = mhd emh))) ∨
(∃T m. t = ArrayT T ∧ G⊢Array T accessible_in (pid S) ∧
accmethd G S Object sig = Some m ∧ accmodi m ≠ Private ∧
declrefT emh = ClassT Object ∧ mhead (mthd m) = mhd emh)"
apply (rule_tac ref_ty1="t" in ref_ty_ty.induct [THEN conjunct1])
apply auto
apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def)
apply (auto dest!: accmethd_SomeD)
done
lemma mheads_cases:
assumes "emh ∈ mheads G S t sig" and "wf_prog G"
obtains (Class_methd) C D m where
"t = ClassT C" "declrefT emh = ClassT D" "accmethd G S C sig = Some m"
"declclass m = D" "mhead (mthd m) = mhd emh"
| (Iface_methd) I im where "t = IfaceT I"
"im ∈ accimethds G (pid S) I sig" "mthd im = mhd emh"
| (Iface_Object_methd) I m where
"t = IfaceT I" "G⊢Iface I accessible_in (pid S)"
"accmethd G S Object sig = Some m" "accmodi m ≠ Private"
"declrefT emh = ClassT Object" "mhead (mthd m) = mhd emh"
| (Array_Object_methd) T m where
"t = ArrayT T" "G⊢Array T accessible_in (pid S)"
"accmethd G S Object sig = Some m" "accmodi m ≠ Private"
"declrefT emh = ClassT Object" "mhead (mthd m) = mhd emh"
using assms by (blast dest!: mheadsD)
lemma declclassD[rule_format]:
"⟦wf_prog G;class G C = Some c; methd G C sig = Some m;
class G (declclass m) = Some d⟧
⟹ table_of (methods d) sig = Some (mthd m)"
proof -
assume wf: "wf_prog G"
then have ws: "ws_prog G" ..
assume clsC: "class G C = Some c"
from clsC ws
show "⋀ m d. ⟦methd G C sig = Some m; class G (declclass m) = Some d⟧
⟹ table_of (methods d) sig = Some (mthd m)"
proof (induct rule: ws_class_induct)
case Object
with wf show "?thesis m d" by auto
next
case (Subcls C c)
let ?newMethods = "table_of (map (λ(s, m). (s, C, m)) (methods c)) sig"
show "?thesis m d"
proof (cases "?newMethods")
case None
from None ws Subcls
show "?thesis" by (auto simp add: methd_rec) (rule Subcls)
next
case Some
from Some ws Subcls
show "?thesis"
by (auto simp add: methd_rec
dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
qed
qed
qed
lemma dynmethd_Object:
assumes statM: "methd G Object sig = Some statM" and
"private": "accmodi statM = Private" and
is_cls_C: "is_class G C" and
wf: "wf_prog G"
shows "dynmethd G Object C sig = Some statM"
proof -
from is_cls_C wf
have subclseq: "G⊢C ≼⇩C Object"
by (auto intro: subcls_ObjectI)
from wf have ws: "ws_prog G"
by simp
from wf
have is_cls_Obj: "is_class G Object"
by simp
from statM subclseq is_cls_Obj ws "private"
show ?thesis
proof (cases rule: dynmethd_cases)
case Static then show ?thesis .
next
case Overrides
with "private" show ?thesis
by (auto dest: no_Private_override)
qed
qed
lemma wf_imethds_hiding_objmethdsD:
assumes old: "methd G Object sig = Some old" and
is_if_I: "is_iface G I" and
wf: "wf_prog G" and
not_private: "accmodi old ≠ Private" and
new: "new ∈ imethds G I sig"
shows "G⊢resTy new≼resTy old ∧ is_static new = is_static old" (is "?P new")
proof -
from wf have ws: "ws_prog G" by simp
{
fix I i new
assume ifI: "iface G I = Some i"
assume new: "table_of (imethods i) sig = Some new"
from ifI new not_private wf old
have "?P (I,new)"
by (auto dest!: wf_prog_idecl wf_idecl_hiding cond_hiding_entailsD
simp del: methd_Object)
} note hyp_newmethod = this
from is_if_I ws new
show ?thesis
proof (induct rule: ws_interface_induct)
case (Step I i)
assume ifI: "iface G I = Some i"
assume new: "new ∈ imethds G I sig"
from Step
have hyp: "∀ J ∈ set (isuperIfs i). (new ∈ imethds G J sig ⟶ ?P new)"
by auto
from new ifI ws
show "?P new"
proof (cases rule: imethds_cases)
case NewMethod
with ifI hyp_newmethod
show ?thesis
by auto
next
case (InheritedMethod J)
assume "J ∈ set (isuperIfs i)"
"new ∈ imethds G J sig"
with hyp
show "?thesis"
by auto
qed
qed
qed
text ‹
Which dynamic classes are valid to look up a member of a distinct static type?
We have to distinct class members (named static members in Java)
from instance members. Class members are global to all Objects of a class,
instance members are local to a single Object instance. If a member is
equipped with the static modifier it is a class member, else it is an
instance member.
The following table gives an overview of the current framework. We assume
to have a reference with static type statT and a dynamic class dynC. Between
both of these types the widening relation holds
\<^term>‹G⊢Class dynC≼ statT›. Unfortunately this ordinary widening relation
isn't enough to describe the valid lookup classes, since we must cope the
special cases of arrays and interfaces,too. If we statically expect an array or
inteface we may lookup a field or a method in Object which isn't covered in
the widening relation.
statT field instance method static (class) method
------------------------------------------------------------------------
NullT / / /
Iface / dynC Object
Class dynC dynC dynC
Array / Object Object
In most cases we con lookup the member in the dynamic class. But as an
interface can't declare new static methods, nor an array can define new
methods at all, we have to lookup methods in the base class Object.
The limitation to classes in the field column is artificial and comes out
of the typing rule for the field access (see rule ‹FVar› in the
welltyping relation \<^term>‹wt› in theory WellType).
I stems out of the fact, that Object
indeed has no non private fields. So interfaces and arrays can actually
have no fields at all and a field access would be senseless. (In Java
interfaces are allowed to declare new fields but in current Bali not!).
So there is no principal reason why we should not allow Objects to declare
non private fields. Then we would get the following column:
statT field
-----------------
NullT /
Iface Object
Class dynC
Array Object
›
primrec valid_lookup_cls:: "prog ⇒ ref_ty ⇒ qtname ⇒ bool ⇒ bool"
("_,_ ⊢ _ valid'_lookup'_cls'_for _" [61,61,61,61] 60)
where
"G,NullT ⊢ dynC valid_lookup_cls_for static_membr = False"
| "G,IfaceT I ⊢ dynC valid_lookup_cls_for static_membr
= (if static_membr
then dynC=Object
else G⊢Class dynC≼ Iface I)"
| "G,ClassT C ⊢ dynC valid_lookup_cls_for static_membr = G⊢Class dynC≼ Class C"
| "G,ArrayT T ⊢ dynC valid_lookup_cls_for static_membr = (dynC=Object)"
lemma valid_lookup_cls_is_class:
assumes dynC: "G,statT ⊢ dynC valid_lookup_cls_for static_membr" and
ty_statT: "isrtype G statT" and
wf: "wf_prog G"
shows "is_class G dynC"
proof (cases statT)
case NullT
with dynC ty_statT show ?thesis
by (auto dest: widen_NT2)
next
case (IfaceT I)
with dynC wf show ?thesis
by (auto dest: implmt_is_class)
next
case (ClassT C)
with dynC ty_statT show ?thesis
by (auto dest: subcls_is_class2)
next
case (ArrayT T)
with dynC wf show ?thesis
by (auto)
qed
declare split_paired_All [simp del] split_paired_Ex [simp del]
setup ‹map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")›
setup ‹map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")›
lemma dynamic_mheadsD:
"⟦emh ∈ mheads G S statT sig;
G,statT ⊢ dynC valid_lookup_cls_for (is_static emh);
isrtype G statT; wf_prog G
⟧ ⟹ ∃m ∈ dynlookup G statT dynC sig:
is_static m=is_static emh ∧ G⊢resTy m≼resTy emh"
proof -
assume emh: "emh ∈ mheads G S statT sig"
and wf: "wf_prog G"
and dynC_Prop: "G,statT ⊢ dynC valid_lookup_cls_for (is_static emh)"
and istype: "isrtype G statT"
from dynC_Prop istype wf
obtain y where
dynC: "class G dynC = Some y"
by (auto dest: valid_lookup_cls_is_class)
from emh wf show ?thesis
proof (cases rule: mheads_cases)
case Class_methd
fix statC statDeclC sm
assume statC: "statT = ClassT statC"
assume "accmethd G S statC sig = Some sm"
then have sm: "methd G statC sig = Some sm"
by (blast dest: accmethd_SomeD)
assume eq_mheads: "mhead (mthd sm) = mhd emh"
from statC
have dynlookup: "dynlookup G statT dynC sig = dynmethd G statC dynC sig"
by (simp add: dynlookup_def)
from wf statC istype dynC_Prop sm
obtain dm where
"dynmethd G statC dynC sig = Some dm"
"is_static dm = is_static sm"
"G⊢resTy dm≼resTy sm"
by (force dest!: ws_dynmethd accmethd_SomeD)
with dynlookup eq_mheads
show ?thesis
by (cases emh type: prod) (auto)
next
case Iface_methd
fix I im
assume statI: "statT = IfaceT I" and
eq_mheads: "mthd im = mhd emh" and
"im ∈ accimethds G (pid S) I sig"
then have im: "im ∈ imethds G I sig"
by (blast dest: accimethdsD)
with istype statI eq_mheads wf
have not_static_emh: "¬ is_static emh"
by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
from statI im
have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
by (auto simp add: dynlookup_def dynimethd_def)
from wf dynC_Prop statI istype im not_static_emh
obtain dm where
"methd G dynC sig = Some dm"
"is_static dm = is_static im"
"G⊢resTy (mthd dm)≼resTy (mthd im)"
by (force dest: implmt_methd)
with dynlookup eq_mheads
show ?thesis
by (cases emh type: prod) (auto)
next
case Iface_Object_methd
fix I sm
assume statI: "statT = IfaceT I" and
sm: "accmethd G S Object sig = Some sm" and
eq_mheads: "mhead (mthd sm) = mhd emh" and
nPriv: "accmodi sm ≠ Private"
show ?thesis
proof (cases "imethds G I sig = {}")
case True
with statI
have dynlookup: "dynlookup G statT dynC sig = dynmethd G Object dynC sig"
by (simp add: dynlookup_def dynimethd_def)
from wf dynC
have subclsObj: "G⊢dynC ≼⇩C Object"
by (auto intro: subcls_ObjectI)
from wf dynC dynC_Prop istype sm subclsObj
obtain dm where
"dynmethd G Object dynC sig = Some dm"
"is_static dm = is_static sm"
"G⊢resTy (mthd dm)≼resTy (mthd sm)"
by (auto dest!: ws_dynmethd accmethd_SomeD
intro: class_Object [OF wf] intro: that)
with dynlookup eq_mheads
show ?thesis
by (cases emh type: prod) (auto)
next
case False
with statI
have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig"
by (simp add: dynlookup_def dynimethd_def)
from istype statI
have "is_iface G I"
by auto
with wf sm nPriv False
obtain im where
im: "im ∈ imethds G I sig" and
eq_stat: "is_static im = is_static sm" and
resProp: "G⊢resTy (mthd im)≼resTy (mthd sm)"
by (auto dest: wf_imethds_hiding_objmethdsD accmethd_SomeD)
from im wf statI istype eq_stat eq_mheads
have not_static_sm: "¬ is_static emh"
by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead)
from im wf dynC_Prop dynC istype statI not_static_sm
obtain dm where
"methd G dynC sig = Some dm"
"is_static dm = is_static im"
"G⊢resTy (mthd dm)≼resTy (mthd im)"
by (auto dest: implmt_methd)
with wf eq_stat resProp dynlookup eq_mheads
show ?thesis
by (cases emh type: prod) (auto intro: widen_trans)
qed
next
case Array_Object_methd
fix T sm
assume statArr: "statT = ArrayT T" and
sm: "accmethd G S Object sig = Some sm" and
eq_mheads: "mhead (mthd sm) = mhd emh"
from statArr dynC_Prop wf
have dynlookup: "dynlookup G statT dynC sig = methd G Object sig"
by (auto simp add: dynlookup_def dynmethd_C_C)
with sm eq_mheads sm
show ?thesis
by (cases emh type: prod) (auto dest: accmethd_SomeD)
qed
qed
declare split_paired_All [simp] split_paired_Ex [simp]
setup ‹map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))›
setup ‹map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))›
lemma methd_declclass:
"⟦class G C = Some c; wf_prog G; methd G C sig = Some m⟧
⟹ methd G (declclass m) sig = Some m"
proof -
assume asm: "class G C = Some c" "wf_prog G" "methd G C sig = Some m"
have "wf_prog G ⟶
(∀ c m. class G C = Some c ⟶ methd G C sig = Some m
⟶ methd G (declclass m) sig = Some m)" (is "?P G C")
proof (induct G C rule: class_rec_induct', intro allI impI)
fix G C c m
assume hyp: "⋀c. class G C = Some c ⟹ ws_prog G ⟹ C ≠ Object ⟹
?P G (super c)"
assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
m: "methd G C sig = Some m"
show "methd G (declclass m) sig = Some m"
proof (cases "C=Object")
case True
with wf m show ?thesis by (auto intro: table_of_map_SomeI)
next
let ?filter="filter_tab (λsig m. G⊢C inherits method sig m)"
let ?table = "table_of (map (λ(s, m). (s, C, m)) (methods c))"
case False
with cls_C wf m
have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
by (simp add: methd_rec)
show ?thesis
proof (cases "?table sig")
case None
from this methd_C have "?filter (methd G (super c)) sig = Some m"
by simp
moreover
from wf cls_C False obtain sup where "class G (super c) = Some sup"
by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
moreover note wf False cls_C
ultimately show ?thesis by (auto intro: hyp [rule_format])
next
case Some
from this methd_C m show ?thesis by auto
qed
qed
qed
with asm show ?thesis by auto
qed
lemma dynmethd_declclass:
"⟦dynmethd G statC dynC sig = Some m;
wf_prog G; is_class G statC
⟧ ⟹ methd G (declclass m) sig = Some m"
by (auto dest: dynmethd_declC)
lemma dynlookup_declC:
"⟦dynlookup G statT dynC sig = Some m; wf_prog G;
is_class G dynC;isrtype G statT
⟧ ⟹ G⊢dynC ≼⇩C (declclass m) ∧ is_class G (declclass m)"
by (cases "statT")
(auto simp add: dynlookup_def dynimethd_def
dest: methd_declC dynmethd_declC)
lemma dynlookup_Array_declclassD [simp]:
"⟦dynlookup G (ArrayT T) Object sig = Some dm;wf_prog G⟧
⟹ declclass dm = Object"
proof -
assume dynL: "dynlookup G (ArrayT T) Object sig = Some dm"
assume wf: "wf_prog G"
from wf have ws: "ws_prog G" by auto
from wf have is_cls_Obj: "is_class G Object" by auto
from dynL wf
show ?thesis
by (auto simp add: dynlookup_def dynmethd_C_C [OF is_cls_Obj ws]
dest: methd_Object_SomeD)
qed
declare split_paired_All [simp del] split_paired_Ex [simp del]
setup ‹map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")›
setup ‹map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")›
lemma wt_is_type: "E,dt⊨v∷T ⟹ wf_prog (prg E) ⟶
dt=empty_dt ⟶ (case T of
Inl T ⇒ is_type (prg E) T
| Inr Ts ⇒ Ball (set Ts) (is_type (prg E)))"
apply (unfold empty_dt_def)
apply (erule wt.induct)
apply (auto split del: if_split_asm simp del: snd_conv
simp add: is_acc_class_def is_acc_type_def)
apply (erule typeof_empty_is_type)
apply (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD],
force simp del: snd_conv, clarsimp simp add: is_acc_class_def)
apply (drule (1) max_spec2mheads [THEN conjunct1, THEN mheadsD])
apply (drule_tac [2] accfield_fields)
apply (frule class_Object)
apply (auto dest: accmethd_rT_is_type
imethds_wf_mhead [THEN conjunct1, THEN rT_is_acc_type]
dest!:accimethdsD
simp del: class_Object
simp add: is_acc_type_def
)
done
declare split_paired_All [simp] split_paired_Ex [simp]
setup ‹map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))›
setup ‹map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))›
lemma ty_expr_is_type:
"⟦E⊢e∷-T; wf_prog (prg E)⟧ ⟹ is_type (prg E) T"
by (auto dest!: wt_is_type)
lemma ty_var_is_type:
"⟦E⊢v∷=T; wf_prog (prg E)⟧ ⟹ is_type (prg E) T"
by (auto dest!: wt_is_type)
lemma ty_exprs_is_type:
"⟦E⊢es∷≐Ts; wf_prog (prg E)⟧ ⟹ Ball (set Ts) (is_type (prg E))"
by (auto dest!: wt_is_type)
lemma static_mheadsD:
"⟦ emh ∈ mheads G S t sig; wf_prog G; E⊢e∷-RefT t; prg E=G ;
invmode (mhd emh) e ≠ IntVir
⟧ ⟹ ∃m. ( (∃ C. t = ClassT C ∧ accmethd G S C sig = Some m)
∨ (∀ C. t ≠ ClassT C ∧ accmethd G S Object sig = Some m )) ∧
declrefT emh = ClassT (declclass m) ∧ mhead (mthd m) = (mhd emh)"
apply (subgoal_tac "is_static emh ∨ e = Super")
defer apply (force simp add: invmode_def)
apply (frule ty_expr_is_type)
apply simp
apply (case_tac "is_static emh")
apply (frule (1) mheadsD)
apply clarsimp
apply safe
apply blast
apply (auto dest!: imethds_wf_mhead
accmethd_SomeD
accimethdsD
simp add: accObjectmheads_def Objectmheads_def)
apply (erule wt_elim_cases)
apply (force simp add: cmheads_def)
done
lemma wt_MethdI:
"⟦methd G C sig = Some m; wf_prog G;
class G C = Some c⟧ ⟹
∃T. ⦇prg=G,cls=(declclass m),
lcl=callee_lcl (declclass m) sig (mthd m)⦈⊢ Methd C sig∷-T ∧ G⊢T≼resTy m"
apply (frule (2) methd_wf_mdecl, clarify)
apply (force dest!: wf_mdecl_bodyD intro!: wt.Methd)
done
subsection "accessibility concerns"
lemma mheads_type_accessible:
"⟦emh ∈ mheads G S T sig; wf_prog G⟧
⟹ G⊢RefT T accessible_in (pid S)"
by (erule mheads_cases)
(auto dest: accmethd_SomeD accessible_from_commonD accimethdsD)
lemma static_to_dynamic_accessible_from_aux:
"⟦G⊢m of C accessible_from accC;wf_prog G⟧
⟹ G⊢m in C dyn_accessible_from accC"
proof (induct rule: accessible_fromR.induct)
qed (auto intro: dyn_accessible_fromR.intros
member_of_to_member_in
static_to_dynamic_overriding)
lemma static_to_dynamic_accessible_from:
assumes stat_acc: "G⊢m of statC accessible_from accC" and
subclseq: "G⊢dynC ≼⇩C statC" and
wf: "wf_prog G"
shows "G⊢m in dynC dyn_accessible_from accC"
proof -
from stat_acc subclseq
show ?thesis (is "?Dyn_accessible m")
proof (induct rule: accessible_fromR.induct)
case (Immediate m statC)
then show "?Dyn_accessible m"
by (blast intro: dyn_accessible_fromR.Immediate
member_inI
permits_acc_inheritance)
next
case (Overriding m _ _)
with wf show "?Dyn_accessible m"
by (blast intro: dyn_accessible_fromR.Overriding
member_inI
static_to_dynamic_overriding
rtrancl_trancl_trancl
static_to_dynamic_accessible_from_aux)
qed
qed
lemma static_to_dynamic_accessible_from_static:
assumes stat_acc: "G⊢m of statC accessible_from accC" and
static: "is_static m" and
wf: "wf_prog G"
shows "G⊢m in (declclass m) dyn_accessible_from accC"
proof -
from stat_acc wf
have "G⊢m in statC dyn_accessible_from accC"
by (auto intro: static_to_dynamic_accessible_from)
from this static
show ?thesis
by (rule dyn_accessible_from_static_declC)
qed
lemma dynmethd_member_in:
assumes m: "dynmethd G statC dynC sig = Some m" and
iscls_statC: "is_class G statC" and
wf: "wf_prog G"
shows "G⊢Methd sig m member_in dynC"
proof -
from m
have subclseq: "G⊢dynC ≼⇩C statC"
by (auto simp add: dynmethd_def)
from subclseq iscls_statC
have iscls_dynC: "is_class G dynC"
by (rule subcls_is_class2)
from iscls_dynC iscls_statC wf m
have "G⊢dynC ≼⇩C (declclass m) ∧ is_class G (declclass m) ∧
methd G (declclass m) sig = Some m"
by - (drule dynmethd_declC, auto)
with wf
show ?thesis
by (auto intro: member_inI dest: methd_member_of)
qed
lemma dynmethd_access_prop:
assumes statM: "methd G statC sig = Some statM" and
stat_acc: "G⊢Methd sig statM of statC accessible_from accC" and
dynM: "dynmethd G statC dynC sig = Some dynM" and
wf: "wf_prog G"
shows "G⊢Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from wf have ws: "ws_prog G" ..
from dynM
have subclseq: "G⊢dynC ≼⇩C statC"
by (auto simp add: dynmethd_def)
from stat_acc
have is_cls_statC: "is_class G statC"
by (auto dest: accessible_from_commonD member_of_is_classD)
with subclseq
have is_cls_dynC: "is_class G dynC"
by (rule subcls_is_class2)
from is_cls_statC statM wf
have member_statC: "G⊢Methd sig statM member_of statC"
by (auto intro: methd_member_of)
from stat_acc
have statC_acc: "G⊢Class statC accessible_in (pid accC)"
by (auto dest: accessible_from_commonD)
from statM subclseq is_cls_statC ws
show ?thesis
proof (cases rule: dynmethd_cases)
case Static
assume dynmethd: "dynmethd G statC dynC sig = Some statM"
with dynM have eq_dynM_statM: "dynM=statM"
by simp
with stat_acc subclseq wf
show ?thesis
by (auto intro: static_to_dynamic_accessible_from)
next
case (Overrides newM)
assume dynmethd: "dynmethd G statC dynC sig = Some newM"
assume override: "G,sig⊢newM overrides statM"
assume neq: "newM≠statM"
from dynmethd dynM
have eq_dynM_newM: "dynM=newM"
by simp
from dynmethd eq_dynM_newM wf is_cls_statC
have "G⊢Methd sig dynM member_in dynC"
by (auto intro: dynmethd_member_in)
moreover
from subclseq
have "G⊢dynC≺⇩C statC"
proof (cases rule: subclseq_cases)
case Eq
assume "dynC=statC"
moreover
from is_cls_statC obtain c
where "class G statC = Some c"
by auto
moreover
note statM ws dynmethd
ultimately
have "newM=statM"
by (auto simp add: dynmethd_C_C)
with neq show ?thesis
by (contradiction)
next
case Subcls then show ?thesis .
qed
moreover
from stat_acc wf
have "G⊢Methd sig statM in statC dyn_accessible_from accC"
by (blast intro: static_to_dynamic_accessible_from)
moreover
note override eq_dynM_newM
ultimately show ?thesis
by (cases dynM,cases statM) (auto intro: dyn_accessible_fromR.Overriding)
qed
qed
lemma implmt_methd_access:
fixes accC::qtname
assumes iface_methd: "imethds G I sig ≠ {}" and
implements: "G⊢dynC↝I" and
isif_I: "is_iface G I" and
wf: "wf_prog G"
shows "∃ dynM. methd G dynC sig = Some dynM ∧
G⊢Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from implements
have iscls_dynC: "is_class G dynC" by (rule implmt_is_class)
from iface_methd
obtain im
where "im ∈ imethds G I sig"
by auto
with wf implements isif_I
obtain dynM
where dynM: "methd G dynC sig = Some dynM" and
pub: "accmodi dynM = Public"
by (blast dest: implmt_methd)
with iscls_dynC wf
have "G⊢Methd sig dynM in dynC dyn_accessible_from accC"
by (auto intro!: dyn_accessible_fromR.Immediate
intro: methd_member_of member_of_to_member_in
simp add: permits_acc_def)
with dynM
show ?thesis
by blast
qed
corollary implmt_dynimethd_access:
fixes accC::qtname
assumes iface_methd: "imethds G I sig ≠ {}" and
implements: "G⊢dynC↝I" and
isif_I: "is_iface G I" and
wf: "wf_prog G"
shows "∃ dynM. dynimethd G I dynC sig = Some dynM ∧
G⊢Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from iface_methd
have "dynimethd G I dynC sig = methd G dynC sig"
by (simp add: dynimethd_def)
with iface_methd implements isif_I wf
show ?thesis
by (simp only:)
(blast intro: implmt_methd_access)
qed
lemma dynlookup_access_prop:
assumes emh: "emh ∈ mheads G accC statT sig" and
dynM: "dynlookup G statT dynC sig = Some dynM" and
dynC_prop: "G,statT ⊢ dynC valid_lookup_cls_for is_static emh" and
isT_statT: "isrtype G statT" and
wf: "wf_prog G"
shows "G ⊢Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from emh wf
have statT_acc: "G⊢RefT statT accessible_in (pid accC)"
by (rule mheads_type_accessible)
from dynC_prop isT_statT wf
have iscls_dynC: "is_class G dynC"
by (rule valid_lookup_cls_is_class)
from emh dynC_prop isT_statT wf dynM
have eq_static: "is_static emh = is_static dynM"
by (auto dest: dynamic_mheadsD)
from emh wf show ?thesis
proof (cases rule: mheads_cases)
case (Class_methd statC _ statM)
assume statT: "statT = ClassT statC"
assume "accmethd G accC statC sig = Some statM"
then have statM: "methd G statC sig = Some statM" and
stat_acc: "G⊢Methd sig statM of statC accessible_from accC"
by (auto dest: accmethd_SomeD)
from dynM statT
have dynM': "dynmethd G statC dynC sig = Some dynM"
by (simp add: dynlookup_def)
from statM stat_acc wf dynM'
show ?thesis
by (auto dest!: dynmethd_access_prop)
next
case (Iface_methd I im)
then have iface_methd: "imethds G I sig ≠ {}" and
statT_acc: "G⊢RefT statT accessible_in (pid accC)"
by (auto dest: accimethdsD)
assume statT: "statT = IfaceT I"
assume im: "im ∈ accimethds G (pid accC) I sig"
assume eq_mhds: "mthd im = mhd emh"
from dynM statT
have dynM': "dynimethd G I dynC sig = Some dynM"
by (simp add: dynlookup_def)
from isT_statT statT
have isif_I: "is_iface G I"
by simp
show ?thesis
proof (cases "is_static emh")
case False
with statT dynC_prop
have widen_dynC: "G⊢Class dynC ≼ RefT statT"
by simp
from statT widen_dynC
have implmnt: "G⊢dynC↝I"
by auto
from eq_static False
have not_static_dynM: "¬ is_static dynM"
by simp
from iface_methd implmnt isif_I wf dynM'
show ?thesis
by - (drule implmt_dynimethd_access, auto)
next
case True
assume "is_static emh"
moreover
from wf isT_statT statT im
have "¬ is_static im"
by (auto dest: accimethdsD wf_prog_idecl imethds_wf_mhead)
moreover note eq_mhds
ultimately show ?thesis
by (cases emh) auto
qed
next
case (Iface_Object_methd I statM)
assume statT: "statT = IfaceT I"
assume "accmethd G accC Object sig = Some statM"
then have statM: "methd G Object sig = Some statM" and
stat_acc: "G⊢Methd sig statM of Object accessible_from accC"
by (auto dest: accmethd_SomeD)
assume not_Private_statM: "accmodi statM ≠ Private"
assume eq_mhds: "mhead (mthd statM) = mhd emh"
from iscls_dynC wf
have widen_dynC_Obj: "G⊢dynC ≼⇩C Object"
by (auto intro: subcls_ObjectI)
show ?thesis
proof (cases "imethds G I sig = {}")
case True
from dynM statT True
have dynM': "dynmethd G Object dynC sig = Some dynM"
by (simp add: dynlookup_def dynimethd_def)
from statT
have "G⊢RefT statT ≼Class Object"
by auto
with statM statT_acc stat_acc widen_dynC_Obj statT isT_statT
wf dynM' eq_static dynC_prop
show ?thesis
by - (drule dynmethd_access_prop,force+)
next
case False
then obtain im where
im: "im ∈ imethds G I sig"
by auto
have not_static_emh: "¬ is_static emh"
proof -
from im statM statT isT_statT wf not_Private_statM
have "is_static im = is_static statM"
by (fastforce dest: wf_imethds_hiding_objmethdsD)
with wf isT_statT statT im
have "¬ is_static statM"
by (auto dest: wf_prog_idecl imethds_wf_mhead)
with eq_mhds
show ?thesis
by (cases emh) auto
qed
with statT dynC_prop
have implmnt: "G⊢dynC↝I"
by simp
with isT_statT statT
have isif_I: "is_iface G I"
by simp
from dynM statT
have dynM': "dynimethd G I dynC sig = Some dynM"
by (simp add: dynlookup_def)
from False implmnt isif_I wf dynM'
show ?thesis
by - (drule implmt_dynimethd_access, auto)
qed
next
case (Array_Object_methd T statM)
assume statT: "statT = ArrayT T"
assume "accmethd G accC Object sig = Some statM"
then have statM: "methd G Object sig = Some statM" and
stat_acc: "G⊢Methd sig statM of Object accessible_from accC"
by (auto dest: accmethd_SomeD)
from statT dynC_prop
have dynC_Obj: "dynC = Object"
by simp
then
have widen_dynC_Obj: "G⊢Class dynC ≼ Class Object"
by simp
from dynM statT
have dynM': "dynmethd G Object dynC sig = Some dynM"
by (simp add: dynlookup_def)
from statM statT_acc stat_acc dynM' wf widen_dynC_Obj
statT isT_statT
show ?thesis
by - (drule dynmethd_access_prop, simp+)
qed
qed
lemma dynlookup_access:
assumes emh: "emh ∈ mheads G accC statT sig" and
dynC_prop: "G,statT ⊢ dynC valid_lookup_cls_for (is_static emh) " and
isT_statT: "isrtype G statT" and
wf: "wf_prog G"
shows "∃ dynM. dynlookup G statT dynC sig = Some dynM ∧
G⊢Methd sig dynM in dynC dyn_accessible_from accC"
proof -
from dynC_prop isT_statT wf
have is_cls_dynC: "is_class G dynC"
by (auto dest: valid_lookup_cls_is_class)
with emh wf dynC_prop isT_statT
obtain dynM where
"dynlookup G statT dynC sig = Some dynM"
by - (drule dynamic_mheadsD,auto)
with emh dynC_prop isT_statT wf
show ?thesis
by (blast intro: dynlookup_access_prop)
qed
lemma stat_overrides_Package_old:
assumes stat_override: "G ⊢ new overrides⇩S old" and
accmodi_new: "accmodi new = Package" and
wf: "wf_prog G "
shows "accmodi old = Package"
proof -
from stat_override wf
have "accmodi old ≤ accmodi new"
by (auto dest: wf_prog_stat_overridesD)
with stat_override accmodi_new show ?thesis
by (cases "accmodi old") (auto dest: no_Private_stat_override
dest: acc_modi_le_Dests)
qed
subsubsection ‹Properties of dynamic accessibility›
lemma dyn_accessible_Private:
assumes dyn_acc: "G ⊢ m in C dyn_accessible_from accC" and
priv: "accmodi m = Private"
shows "accC = declclass m"
proof -
from dyn_acc priv
show ?thesis
proof (induct)
case (Immediate m C)
from ‹G ⊢ m in C permits_acc_from accC› and ‹accmodi m = Private›
show ?case
by (simp add: permits_acc_def)
next
case Overriding
then show ?case
by (auto dest!: overrides_commonD)
qed
qed
text ‹‹dyn_accessible_Package› only works with the ‹wf_prog› assumption.
Without it. it is easy to leaf the Package!
›
lemma dyn_accessible_Package:
"⟦G ⊢ m in C dyn_accessible_from accC; accmodi m = Package;
wf_prog G⟧
⟹ pid accC = pid (declclass m)"
proof -
assume wf: "wf_prog G "
assume accessible: "G ⊢ m in C dyn_accessible_from accC"
then show "accmodi m = Package
⟹ pid accC = pid (declclass m)"
(is "?Pack m ⟹ ?P m")
proof (induct rule: dyn_accessible_fromR.induct)
case (Immediate m C)
assume "G⊢m member_in C"
"G ⊢ m in C permits_acc_from accC"
"accmodi m = Package"
then show "?P m"
by (auto simp add: permits_acc_def)
next
case (Overriding new declC newm old Sup C)
assume member_new: "G ⊢ new member_in C" and
new: "new = (declC, mdecl newm)" and
override: "G ⊢ (declC, newm) overrides old" and
subcls_C_Sup: "G⊢C ≺⇩C Sup" and
acc_old: "G ⊢ methdMembr old in Sup dyn_accessible_from accC" and
hyp: "?Pack (methdMembr old) ⟹ ?P (methdMembr old)" and
accmodi_new: "accmodi new = Package"
from override accmodi_new new wf
have accmodi_old: "accmodi old = Package"
by (auto dest: overrides_Package_old)
with hyp
have P_sup: "?P (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: dyn_override_Package)
with eq_pid_new_old P_sup show "?P new"
by auto
qed
qed
text ‹For fields we don't need the wellformedness of the program, since
there is no overriding›
lemma dyn_accessible_field_Package:
assumes dyn_acc: "G ⊢ f in C dyn_accessible_from accC" and
pack: "accmodi f = Package" and
field: "is_field f"
shows "pid accC = pid (declclass f)"
proof -
from dyn_acc pack field
show ?thesis
proof (induct)
case (Immediate f C)
from ‹G ⊢ f in C permits_acc_from accC› and ‹accmodi f = Package›
show ?case
by (simp add: permits_acc_def)
next
case Overriding
then show ?case by (simp add: is_field_def)
qed
qed
text ‹‹dyn_accessible_instance_field_Protected› only works for fields
since methods can break the package bounds due to overriding
›
lemma dyn_accessible_instance_field_Protected:
assumes dyn_acc: "G ⊢ f in C dyn_accessible_from accC" and
prot: "accmodi f = Protected" and
field: "is_field f" and
instance_field: "¬ is_static f" and
outside: "pid (declclass f) ≠ pid accC"
shows "G⊢ C ≼⇩C accC"
proof -
from dyn_acc prot field instance_field outside
show ?thesis
proof (induct)
case (Immediate f C)
note ‹G ⊢ f in C permits_acc_from accC›
moreover
assume "accmodi f = Protected" and "is_field f" and "¬ is_static f" and
"pid (declclass f) ≠ pid accC"
ultimately
show "G⊢ C ≼⇩C accC"
by (auto simp add: permits_acc_def)
next
case Overriding
then show ?case by (simp add: is_field_def)
qed
qed
lemma dyn_accessible_static_field_Protected:
assumes dyn_acc: "G ⊢ f in C dyn_accessible_from accC" and
prot: "accmodi f = Protected" and
field: "is_field f" and
static_field: "is_static f" and
outside: "pid (declclass f) ≠ pid accC"
shows "G⊢ accC ≼⇩C declclass f ∧ G⊢C ≼⇩C declclass f"
proof -
from dyn_acc prot field static_field outside
show ?thesis
proof (induct)
case (Immediate f C)
assume "accmodi f = Protected" and "is_field f" and "is_static f" and
"pid (declclass f) ≠ pid accC"
moreover
note ‹G ⊢ f in C permits_acc_from accC›
ultimately
have "G⊢ accC ≼⇩C declclass f"
by (auto simp add: permits_acc_def)
moreover
from ‹G ⊢ f member_in C›
have "G⊢C ≼⇩C declclass f"
by (rule member_in_class_relation)
ultimately show ?case
by blast
next
case Overriding
then show ?case by (simp add: is_field_def)
qed
qed
end