Theory WellForm
section ‹Generic Well-formedness of programs›
theory WellForm
imports
SystemClasses
ExternalCall
begin
text ‹\noindent This theory defines global well-formedness conditions
for programs but does not look inside method bodies. Hence it works
for both Jinja and JVM programs. Well-typing of expressions is defined
elsewhere (in theory ‹WellType›).
Because JinjaThreads does not have method overloading, its policy for method
overriding is the classical one: \emph{covariant in the result type
but contravariant in the argument types.} This means the result type
of the overriding method becomes more specific, the argument types
become more general.
›
type_synonym 'm wf_mdecl_test = "'m prog ⇒ cname ⇒ 'm mdecl ⇒ bool"
definition wf_fdecl :: "'m prog ⇒ fdecl ⇒ bool"
where "wf_fdecl P ≡ λ(F,T,fm). is_type P T"
definition wf_mdecl :: "'m wf_mdecl_test ⇒ 'm prog ⇒ cname ⇒ 'm mdecl' ⇒ bool" where
"wf_mdecl wf_md P C ≡
λ(M,Ts,T,m). (∀T∈set Ts. is_type P T) ∧ is_type P T ∧
(case m of Native ⇒ C∙M(Ts) :: T | ⌊mb⌋ ⇒ wf_md P C (M,Ts,T,mb))"
fun wf_overriding :: "'m prog ⇒ cname ⇒ 'm mdecl' ⇒ bool"
where
"wf_overriding P D (M,Ts,T,m) =
(∀D' Ts' T' m'. P ⊢ D sees M:Ts' → T' = m' in D' ⟶ P ⊢ Ts' [≤] Ts ∧ P ⊢ T ≤ T')"
definition wf_cdecl :: "'m wf_mdecl_test ⇒ 'm prog ⇒ 'm cdecl ⇒ bool"
where
"wf_cdecl wf_md P ≡ λ(C,(D,fs,ms)).
(∀f∈set fs. wf_fdecl P f) ∧ distinct_fst fs ∧
(∀m∈set ms. wf_mdecl wf_md P C m) ∧
distinct_fst ms ∧
(C ≠ Object ⟶
is_class P D ∧ ¬ P ⊢ D ≼⇧* C ∧
(∀m∈set ms. wf_overriding P D m)) ∧
(C = Thread ⟶ (∃m. (run, [], Void, m) ∈ set ms))"
definition wf_prog :: "'m wf_mdecl_test ⇒ 'm prog ⇒ bool"
where
"wf_prog wf_md P ⟷ wf_syscls P ∧ distinct_fst (classes P) ∧ (∀c ∈ set (classes P). wf_cdecl wf_md P c)"
lemma wf_prog_def2:
"wf_prog wf_md P ⟷ wf_syscls P ∧ (∀C rest. class P C = ⌊rest⌋ ⟶ wf_cdecl wf_md P (C, rest)) ∧ distinct_fst (classes P)"
by(cases P)(auto simp add: wf_prog_def dest: map_of_SomeD map_of_SomeI)
subsection‹Well-formedness lemmas›
lemma wf_prog_wf_syscls: "wf_prog wf_md P ⟹ wf_syscls P"
by(simp add: wf_prog_def)
lemma class_wf:
"⟦class P C = Some c; wf_prog wf_md P⟧ ⟹ wf_cdecl wf_md P (C,c)"
by (cases P) (fastforce dest: map_of_SomeD simp add: wf_prog_def)
lemma [simp]:
assumes "wf_prog wf_md P"
shows class_Object: "∃C fs ms. class P Object = Some (C,fs,ms)"
and class_Thread: "∃C fs ms. class P Thread = Some (C,fs,ms)"
using wf_prog_wf_syscls[OF assms]
by(rule wf_syscls_class_Object wf_syscls_class_Thread)+
lemma [simp]:
assumes "wf_prog wf_md P"
shows is_class_Object: "is_class P Object"
and is_class_Thread: "is_class P Thread"
using wf_prog_wf_syscls[OF assms] by simp_all
lemma xcpt_subcls_Throwable:
"⟦ C ∈ sys_xcpts; wf_prog wf_md P ⟧ ⟹ P ⊢ C ≼⇧* Throwable"
by(simp add: wf_prog_wf_syscls wf_syscls_xcpt_subcls_Throwable)
lemma is_class_Throwable:
"wf_prog wf_md P ⟹ is_class P Throwable"
by(rule wf_prog_wf_syscls wf_syscls_is_class_Throwable)+
lemma is_class_sub_Throwable:
"⟦ wf_prog wf_md P; P ⊢ C ≼⇧* Throwable ⟧ ⟹ is_class P C"
by(rule wf_syscls_is_class_sub_Throwable[OF wf_prog_wf_syscls])
lemma is_class_xcpt:
"⟦ C ∈ sys_xcpts; wf_prog wf_md P ⟧ ⟹ is_class P C"
by(rule wf_syscls_is_class_xcpt[OF _ wf_prog_wf_syscls])
context heap_base begin
lemma wf_preallocatedE:
assumes "wf_prog wf_md P"
and "preallocated h"
and "C ∈ sys_xcpts"
obtains "typeof_addr h (addr_of_sys_xcpt C) = ⌊Class_type C⌋" "P ⊢ C ≼⇧* Throwable"
proof -
from ‹preallocated h› ‹C ∈ sys_xcpts› have "typeof_addr h (addr_of_sys_xcpt C) = ⌊Class_type C⌋"
by(rule typeof_addr_sys_xcp)
moreover from ‹C ∈ sys_xcpts› ‹wf_prog wf_md P› have "P ⊢ C ≼⇧* Throwable" by(rule xcpt_subcls_Throwable)
ultimately show thesis by(rule that)
qed
lemma wf_preallocatedD:
assumes "wf_prog wf_md P"
and "preallocated h"
and "C ∈ sys_xcpts"
shows "typeof_addr h (addr_of_sys_xcpt C) = ⌊Class_type C⌋ ∧ P ⊢ C ≼⇧* Throwable"
using assms
by(rule wf_preallocatedE) blast
end
lemma (in heap_conf) hconf_start_heap:
"wf_prog wf_md P ⟹ hconf start_heap"
unfolding start_heap_def start_heap_data_def initialization_list_def sys_xcpts_list_def
using hconf_empty
by -(simp add: create_initial_object_simps del: hconf_empty, clarsimp split: prod.split elim!: not_empty_pairE simp del: hconf_empty, drule (1) allocate_Eps, drule (1) hconf_allocate_mono, simp add: is_class_xcpt)+
lemma subcls1_wfD:
"⟦ P ⊢ C ≺⇧1 D; wf_prog wf_md P ⟧ ⟹ D ≠ C ∧ ¬ (subcls1 P)⇧+⇧+ D C"
apply( frule tranclp.r_into_trancl[where r="subcls1 P"])
apply( drule subcls1D)
apply(clarify)
apply( drule (1) class_wf)
apply( unfold wf_cdecl_def)
apply(rule conjI)
apply(force)
apply(unfold reflclp_tranclp[symmetric, where r="subcls1 P"])
apply(blast)
done
lemma wf_cdecl_supD:
"⟦wf_cdecl wf_md P (C,D,r); C ≠ Object⟧ ⟹ is_class P D"
by (auto simp: wf_cdecl_def)
lemma subcls_asym:
"⟦ wf_prog wf_md P; (subcls1 P)⇧+⇧+ C D ⟧ ⟹ ¬ (subcls1 P)⇧+⇧+ D C"
apply(erule tranclp.cases)
apply(fast dest!: subcls1_wfD )
apply(fast dest!: subcls1_wfD intro: tranclp_trans)
done
lemma subcls_irrefl:
"⟦ wf_prog wf_md P; (subcls1 P)⇧+⇧+ C D⟧ ⟹ C ≠ D"
apply (erule tranclp_trans_induct)
apply (auto dest: subcls1_wfD subcls_asym)
done
lemma acyclicP_def:
"acyclicP r ⟷ (∀x. ¬ r^++ x x)"
unfolding acyclic_def trancl_def
by(auto)
lemma acyclic_subcls1:
"wf_prog wf_md P ⟹ acyclicP (subcls1 P)"
by(unfold acyclicP_def)(fast dest: subcls_irrefl)
lemma finite_conversep: "finite {(x, y). r¯¯ x y} = finite {(x, y). r x y}"
by(subst finite_converse[unfolded converse_unfold, symmetric]) simp
lemma acyclicP_wf_subcls1:
"acyclicP (subcls1 P) ⟹ wfP ((subcls1 P)¯¯)"
unfolding wfP_def
by(rule finite_acyclic_wf)(simp_all only: finite_conversep finite_subcls1 acyclicP_converse)
lemma wf_subcls1:
"wf_prog wf_md P ⟹ wfP ((subcls1 P)¯¯)"
by(rule acyclicP_wf_subcls1)(rule acyclic_subcls1)
lemma single_valued_subcls1:
"wf_prog wf_md G ⟹ single_valuedp (subcls1 G)"
by(auto simp:wf_prog_def distinct_fst_def single_valuedp_def dest!:subcls1D)
lemma subcls_induct:
"⟦ wf_prog wf_md P; ⋀C. ∀D. (subcls1 P)⇧+⇧+ C D ⟶ Q D ⟹ Q C ⟧ ⟹ Q C"
(is "?A ⟹ PROP ?P ⟹ _")
proof -
assume p: "PROP ?P"
assume ?A thus ?thesis apply -
apply(drule wf_subcls1)
apply(drule wfP_trancl)
apply(simp only: tranclp_converse)
apply(erule_tac a = C in wfP_induct)
apply(rule p)
apply(auto)
done
qed
lemma subcls1_induct_aux:
"⟦ is_class P C; wf_prog wf_md P; Q Object;
⋀C D fs ms.
⟦ C ≠ Object; is_class P C; class P C = Some (D,fs,ms) ∧
wf_cdecl wf_md P (C,D,fs,ms) ∧ P ⊢ C ≺⇧1 D ∧ is_class P D ∧ Q D⟧ ⟹ Q C ⟧
⟹ Q C"
(is "?A ⟹ ?B ⟹ ?C ⟹ PROP ?P ⟹ _")
proof -
assume p: "PROP ?P"
assume ?A ?B ?C thus ?thesis apply -
apply(unfold is_class_def)
apply( rule impE)
prefer 2
apply( assumption)
prefer 2
apply( assumption)
apply( erule thin_rl)
apply( rule subcls_induct)
apply( assumption)
apply( rule impI)
apply( case_tac "C = Object")
apply( fast)
apply safe
apply( frule (1) class_wf)
apply( frule (1) wf_cdecl_supD)
apply( subgoal_tac "P ⊢ C ≺⇧1 a")
apply( erule_tac [2] subcls1I)
apply( rule p)
apply (unfold is_class_def)
apply auto
done
qed
lemma subcls1_induct [consumes 2, case_names Object Subcls]:
"⟦ wf_prog wf_md P; is_class P C; Q Object;
⋀C D. ⟦C ≠ Object; P ⊢ C ≺⇧1 D; is_class P D; Q D⟧ ⟹ Q C ⟧
⟹ Q C"
apply (erule subcls1_induct_aux, assumption, assumption)
apply blast
done
lemma subcls_C_Object:
"⟦ is_class P C; wf_prog wf_md P ⟧ ⟹ P ⊢ C ≼⇧* Object"
apply(erule (1) subcls1_induct)
apply( fast)
apply(erule (1) converse_rtranclp_into_rtranclp)
done
lemma converse_subcls_is_class:
assumes wf: "wf_prog wf_md P"
shows "⟦ P ⊢ C ≼⇧* D; is_class P C ⟧ ⟹ is_class P D"
proof(induct rule: rtranclp_induct)
assume "is_class P C"
thus "is_class P C" .
next
fix D E
assume PDE: "P ⊢ D ≺⇧1 E"
and IH: "is_class P C ⟹ is_class P D"
and iPC: "is_class P C"
have "is_class P D" by (rule IH[OF iPC])
with PDE obtain fsD MsD where classD: "class P D = ⌊(E, fsD, MsD)⌋"
by(auto simp add: is_class_def elim!: subcls1.cases)
thus "is_class P E" using wf PDE
by(auto elim!: subcls1.cases dest: class_wf simp: wf_cdecl_def)
qed
lemma is_class_is_subcls:
"wf_prog m P ⟹ is_class P C = P ⊢ C ≼⇧* Object"
by (fastforce simp:is_class_def
elim: subcls_C_Object converse_rtranclpE subcls1I
dest: subcls1D)
lemma subcls_antisym:
"⟦wf_prog m P; P ⊢ C ≼⇧* D; P ⊢ D ≼⇧* C⟧ ⟹ C = D"
apply(drule acyclic_subcls1)
apply(drule acyclic_impl_antisym_rtrancl)
apply(drule antisymD)
apply(unfold Transitive_Closure.rtrancl_def)
apply(auto)
done
lemma is_type_pTs:
"⟦ wf_prog wf_md P; class P C = ⌊(S,fs,ms)⌋; (M,Ts,T,m) ∈ set ms ⟧ ⟹ set Ts ⊆ types P"
by(fastforce dest: class_wf simp add: wf_cdecl_def wf_mdecl_def)
lemma widen_asym_1:
assumes wfP: "wf_prog wf_md P"
shows "P ⊢ C ≤ D ⟹ C = D ∨ ¬ (P ⊢ D ≤ C)"
proof (erule widen.induct)
fix T
show "T = T ∨ ¬ (P ⊢ T ≤ T)" by simp
next
fix C D
assume CscD: "P ⊢ C ≼⇧* D"
then have CpscD: "C = D ∨ (C ≠ D ∧ (subcls1 P)⇧+⇧+ C D)" by (simp add: rtranclpD)
{ assume "P ⊢ D ≼⇧* C"
then have DpscC: "D = C ∨ (D ≠ C ∧ (subcls1 P)⇧+⇧+ D C)" by (simp add: rtranclpD)
{ assume "(subcls1 P)⇧+⇧+ D C"
with wfP have CnscD: "¬ (subcls1 P)⇧+⇧+ C D" by (rule subcls_asym)
with CpscD have "C = D" by simp
}
with DpscC have "C = D" by blast
}
hence "Class C = Class D ∨ ¬ (P ⊢ D ≼⇧* C)" by blast
thus "Class C = Class D ∨ ¬ P ⊢ Class D ≤ Class C" by simp
next
fix C
show "NT = Class C ∨ ¬ P ⊢ Class C ≤ NT" by simp
next
fix A
{ assume "P ⊢ A⌊⌉ ≤ NT"
hence "A⌊⌉ = NT" by fastforce
hence "False" by simp }
hence "¬ (P ⊢ A⌊⌉ ≤ NT)" by blast
thus "NT = A⌊⌉ ∨ ¬ P ⊢ A⌊⌉ ≤ NT" by simp
next
fix A
show "A⌊⌉ = Class Object ∨ ¬ P ⊢ Class Object ≤ A⌊⌉"
by(auto dest: Object_widen)
next
fix A B
assume AsU: "P ⊢ A ≤ B" and BnpscA: "A = B ∨ ¬ P ⊢ B ≤ A"
{ assume "P ⊢ B⌊⌉ ≤ A⌊⌉"
hence "P ⊢ B ≤ A" by (auto dest: Array_Array_widen)
with BnpscA have "A = B" by blast
hence "A⌊⌉ = B⌊⌉" by simp }
thus "A⌊⌉ = B⌊⌉ ∨ ¬ P ⊢ B⌊⌉ ≤ A⌊⌉" by blast
qed
lemma widen_asym: "⟦ wf_prog wf_md P; P ⊢ C ≤ D; C ≠ D ⟧ ⟹ ¬ (P ⊢ D ≤ C)"
proof -
assume wfP: "wf_prog wf_md P" and CsD: "P ⊢ C ≤ D" and CneqD: "C ≠ D"
from wfP CsD have "C = D ∨ ¬ (P ⊢ D ≤ C)" by (rule widen_asym_1)
with CneqD show ?thesis by simp
qed
lemma widen_antisym:
"⟦ wf_prog m P; P ⊢ T ≤ U; P ⊢ U ≤ T ⟧ ⟹ T = U"
by(auto dest: widen_asym)
lemma widen_C_Object: "⟦ wf_prog wf_md P; is_class P C ⟧ ⟹ P ⊢ Class C ≤ Class Object"
by(simp add: subcls_C_Object)
lemma is_refType_widen_Object:
assumes wfP: "wf_prog wfmc P"
shows "⟦ is_type P A; is_refT A ⟧ ⟹ P ⊢ A ≤ Class Object"
by(induct A)(auto elim: refTE intro: subcls_C_Object[OF _ wfP] widen_array_object)
lemma is_lub_unique:
assumes wf: "wf_prog wf_md P"
shows "⟦ P ⊢ lub(U, V) = T; P ⊢ lub(U, V) = T' ⟧ ⟹ T = T'"
by(auto elim!: is_lub.cases intro: widen_antisym[OF wf])
subsection‹Well-formedness and method lookup›
lemma sees_wf_mdecl:
"⟦ wf_prog wf_md P; P ⊢ C sees M:Ts→T = m in D ⟧ ⟹ wf_mdecl wf_md P D (M,Ts,T,m)"
apply(drule visible_method_exists)
apply(clarify)
apply(drule class_wf, assumption)
apply(drule map_of_SomeD)
apply(auto simp add: wf_cdecl_def)
done
lemma sees_method_mono [rule_format (no_asm)]:
"⟦ P ⊢ C' ≼⇧* C; wf_prog wf_md P ⟧ ⟹
∀D Ts T m. P ⊢ C sees M:Ts→T = m in D ⟶
(∃D' Ts' T' m'. P ⊢ C' sees M:Ts'→T' = m' in D' ∧ P ⊢ Ts [≤] Ts' ∧ P ⊢ T' ≤ T)"
apply( drule rtranclpD)
apply( erule disjE)
apply( fastforce intro: widen_refl widens_refl)
apply( erule conjE)
apply( erule tranclp_trans_induct)
prefer 2
apply( clarify)
apply( drule spec, drule spec, drule spec, drule spec, erule (1) impE)
apply clarify
apply( fast elim: widen_trans widens_trans)
apply( clarify)
apply( drule subcls1D)
apply( clarify)
apply(clarsimp simp:Method_def)
apply(frule (2) sees_methods_rec)
apply(rule refl)
apply(case_tac "map_of ms M")
apply(rule_tac x = D in exI)
apply(rule_tac x = Ts in exI)
apply(rule_tac x = T in exI)
apply(clarsimp simp add: widens_refl)
apply(rule_tac x = m in exI)
apply(fastforce simp add:map_add_def split:option.split)
apply clarsimp
apply(rename_tac Ts' T' m')
apply( drule (1) class_wf)
apply( unfold wf_cdecl_def Method_def)
apply( frule map_of_SomeD)
apply(clarsimp)
apply(drule (1) bspec)+
apply clarsimp
apply(erule_tac x=D in allE)
apply(erule_tac x=Ts in allE)
apply(rotate_tac -1)
apply(erule_tac x=T in allE)
apply(fastforce simp:map_add_def Method_def split:option.split)
done
lemma sees_method_mono2:
"⟦ P ⊢ C' ≼⇧* C; wf_prog wf_md P;
P ⊢ C sees M:Ts→T = m in D; P ⊢ C' sees M:Ts'→T' = m' in D' ⟧
⟹ P ⊢ Ts [≤] Ts' ∧ P ⊢ T' ≤ T"
by(blast dest:sees_method_mono sees_method_fun)
lemma mdecls_visible:
assumes wf: "wf_prog wf_md P" and "class": "is_class P C"
shows "⋀D fs ms. class P C = Some(D,fs,ms)
⟹ ∃Mm. P ⊢ C sees_methods Mm ∧ (∀(M,Ts,T,m) ∈ set ms. Mm M = Some((Ts,T,m),C))"
using wf "class"
proof (induct rule:subcls1_induct)
case Object
with wf have "distinct_fst ms"
by(auto dest: class_wf simp add: wf_cdecl_def)
with Object show ?case by(fastforce intro!: sees_methods_Object map_of_SomeI)
next
case Subcls
with wf have "distinct_fst ms"
by(auto dest: class_wf simp add: wf_cdecl_def)
with Subcls show ?case
by(fastforce elim:sees_methods_rec dest:subcls1D map_of_SomeI
simp:is_class_def)
qed
lemma mdecl_visible:
assumes wf: "wf_prog wf_md P" and C: "class P C = ⌊(S,fs,ms)⌋" and m: "(M,Ts,T,m) ∈ set ms"
shows "P ⊢ C sees M:Ts→T = m in C"
proof -
from C have "is_class P C" by(auto simp:is_class_def)
with assms show ?thesis
by(bestsimp simp:Method_def dest:mdecls_visible)
qed
lemma sees_wf_native:
"⟦ wf_prog wf_md P; P ⊢ C sees M:Ts→T=Native in D ⟧ ⟹ D∙M(Ts) :: T"
apply(drule (1) sees_wf_mdecl)
apply(simp add: wf_mdecl_def)
done
lemma Call_lemma:
"⟦ P ⊢ C sees M:Ts→T = m in D; P ⊢ C' ≼⇧* C; wf_prog wf_md P ⟧
⟹ ∃D' Ts' T' m'.
P ⊢ C' sees M:Ts'→T' = m' in D' ∧ P ⊢ Ts [≤] Ts' ∧ P ⊢ T' ≤ T ∧ P ⊢ C' ≼⇧* D'
∧ is_type P T' ∧ (∀T∈set Ts'. is_type P T) ∧ (m' ≠ Native ⟶ wf_md P D' (M,Ts',T',the m'))"
apply(frule (2) sees_method_mono)
apply(fastforce intro:sees_method_decl_above dest:sees_wf_mdecl
simp: wf_mdecl_def)
done
lemma sub_Thread_sees_run:
assumes wf: "wf_prog wf_md P"
and PCThread: "P ⊢ C ≼⇧* Thread"
shows "∃D mthd. P ⊢ C sees run: []→Void = ⌊mthd⌋ in D"
proof -
from class_Thread[OF wf] obtain T' fsT MsT
where classT: "class P Thread = ⌊(T', fsT, MsT)⌋" by blast
hence wfcThread: "wf_cdecl wf_md P (Thread, T', fsT, MsT)" using wf by(rule class_wf)
then obtain mrunT where runThread: "(run, [], Void, mrunT) ∈ set MsT"
by(auto simp add: wf_cdecl_def)
moreover have "∃MmT. P ⊢ Thread sees_methods MmT ∧
(∀(M,Ts,T,m) ∈ set MsT. MmT M = Some((Ts,T,m),Thread))"
by(rule mdecls_visible[OF wf is_class_Thread[OF wf] classT])
then obtain MmT where ThreadMmT: "P ⊢ Thread sees_methods MmT"
and MmT: "∀(M,Ts,T,m) ∈ set MsT. MmT M = Some((Ts,T,m),Thread)"
by blast
ultimately obtain mthd
where "MmT run = ⌊(([], Void, mthd), Thread)⌋"
by(fastforce)
with ThreadMmT have Tseesrun: "P ⊢ Thread sees run: []→Void = mthd in Thread"
by(auto simp add: Method_def)
from sees_method_mono[OF PCThread wf Tseesrun]
obtain D' m' where "P ⊢ C sees run: []→Void = m' in D'" by auto
moreover have "m' ≠ None"
proof
assume "m' = None"
with wf ‹P ⊢ C sees run: []→Void = m' in D'› have "D'∙run([]) :: Void"
by(auto intro: sees_wf_native)
thus False by cases auto
qed
ultimately show ?thesis by auto
qed
lemma wf_prog_lift:
assumes wf: "wf_prog (λP C bd. A P C bd) P"
and rule:
"⋀wf_md C M Ts C T m.
⟦ wf_prog wf_md P; P ⊢ C sees M:Ts→T = ⌊m⌋ in C; is_class P C; set Ts ⊆ types P; A P C (M,Ts,T,m) ⟧
⟹ B P C (M,Ts,T,m)"
shows "wf_prog (λP C bd. B P C bd) P"
proof(cases P)
case (Program P')
thus ?thesis using wf
apply(clarsimp simp add: wf_prog_def wf_cdecl_def)
apply(drule (1) bspec)
apply(rename_tac C D fs ms)
apply(subgoal_tac "is_class P C")
prefer 2
apply(simp add: is_class_def)
apply(drule weak_map_of_SomeI)
apply(simp add: Program)
apply(clarsimp simp add: Program wf_mdecl_def split del: option.split)
apply(drule (1) bspec)
apply clarsimp
apply(rule conjI)
apply clarsimp
apply clarsimp
apply(frule (1) map_of_SomeI)
apply(rule rule[OF wf, unfolded Program])
apply(clarsimp simp add: is_class_def)
apply(rule mdecl_visible[OF wf[unfolded Program]])
apply(fastforce intro: is_type_pTs [OF wf, unfolded Program])+
done
qed
subsection‹Well-formedness and field lookup›
lemma wf_Fields_Ex:
"⟦ wf_prog wf_md P; is_class P C ⟧ ⟹ ∃FDTs. P ⊢ C has_fields FDTs"
apply(frule class_Object)
apply(erule (1) subcls1_induct)
apply(blast intro:has_fields_Object)
apply(blast intro:has_fields_rec dest:subcls1D)
done
lemma has_fields_types:
"⟦ P ⊢ C has_fields FDTs; (FD, T, fm) ∈ set FDTs; wf_prog wf_md P ⟧ ⟹ is_type P T"
apply(induct rule:Fields.induct)
apply(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
apply(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)
done
lemma sees_field_is_type:
"⟦ P ⊢ C sees F:T (fm) in D; wf_prog wf_md P ⟧ ⟹ is_type P T"
by(fastforce simp: sees_field_def
elim: has_fields_types map_of_SomeD[OF map_of_remap_SomeD])
lemma wf_has_field_mono2:
assumes wf: "wf_prog wf_md P"
and has: "P ⊢ C has F:T (fm) in E"
shows "⟦ P ⊢ C ≼⇧* D; P ⊢ D ≼⇧* E ⟧ ⟹ P ⊢ D has F:T (fm) in E"
proof(induct rule: rtranclp_induct)
case base show ?case using has .
next
case (step D D')
note DsubD' = ‹P ⊢ D ≺⇧1 D'›
from DsubD' obtain rest where classD: "class P D = ⌊(D', rest)⌋"
and DObj: "D ≠ Object" by(auto elim!: subcls1.cases)
from DsubD' ‹P ⊢ D' ≼⇧* E› have DsubE: "P ⊢ D ≼⇧* E" and DsubE2: "(subcls1 P)^++ D E"
by(rule converse_rtranclp_into_rtranclp rtranclp_into_tranclp2)+
from wf DsubE2 have DnE: "D ≠ E" by(rule subcls_irrefl)
from DsubE have hasD: "P ⊢ D has F:T (fm) in E" by(rule ‹P ⊢ D ≼⇧* E ⟹ P ⊢ D has F:T (fm) in E›)
then obtain FDTs where hasf: "P ⊢ D has_fields FDTs" and FE: "map_of FDTs (F, E) = ⌊(T, fm)⌋"
unfolding has_field_def by blast
from hasf show ?case
proof cases
case has_fields_Object with DObj show ?thesis by simp
next
case (has_fields_rec DD' fs ms FDTs')
with classD have [simp]: "DD' = D'" "rest = (fs, ms)"
and hasf': "P ⊢ D' has_fields FDTs'"
and FDTs: "FDTs = map (λ(F, Tm). ((F, D), Tm)) fs @ FDTs'" by auto
from FDTs FE DnE hasf' show ?thesis by(auto dest: map_of_SomeD simp add: has_field_def)
qed
qed
lemma wf_has_field_idemp:
"⟦ wf_prog wf_md P; P ⊢ C has F:T (fm) in D ⟧ ⟹ P ⊢ D has F:T (fm) in D"
apply(frule has_field_decl_above)
apply(erule (2) wf_has_field_mono2)
apply(rule rtranclp.rtrancl_refl)
done
lemma map_of_remap_conv:
"⟦ distinct_fst fs; map_of (map (λ(F, y). ((F, D), y)) fs) (F, D) = ⌊T⌋ ⟧
⟹ map_of (map (λ((F, D), T). (F, D, T)) (map (λ(F, y). ((F, D), y)) fs)) F = ⌊(D, T)⌋"
apply(induct fs)
apply auto
done
lemma has_field_idemp_sees_field:
assumes wf: "wf_prog wf_md P"
and has: "P ⊢ D has F:T (fm) in D"
shows "P ⊢ D sees F:T (fm) in D"
proof -
from has obtain FDTs where hasf: "P ⊢ D has_fields FDTs"
and FD: "map_of FDTs (F, D) = ⌊(T, fm)⌋" unfolding has_field_def by blast
from hasf have "map_of (map (λ((F, D), T). (F, D, T)) FDTs) F = ⌊(D, T, fm)⌋"
proof cases
case (has_fields_Object D' fs ms)
from ‹class P Object = ⌊(D', fs, ms)⌋› wf
have "wf_cdecl wf_md P (Object, D', fs, ms)" by(rule class_wf)
hence "distinct_fst fs" by(simp add: wf_cdecl_def)
with FD has_fields_Object show ?thesis by(auto intro: map_of_remap_conv simp del: map_map)
next
case (has_fields_rec D' fs ms FDTs')
hence [simp]: "FDTs = map (λ(F, Tm). ((F, D), Tm)) fs @ FDTs'"
and classD: "class P D = ⌊(D', fs, ms)⌋" and DnObj: "D ≠ Object"
and hasf': "P ⊢ D' has_fields FDTs'" by auto
from ‹class P D = ⌊(D', fs, ms)⌋› wf
have "wf_cdecl wf_md P (D, D', fs, ms)" by(rule class_wf)
hence "distinct_fst fs" by(simp add: wf_cdecl_def)
moreover have "map_of FDTs' (F, D) = None"
proof(rule ccontr)
assume "map_of FDTs' (F, D) ≠ None"
then obtain T' fm' where "map_of FDTs' (F, D) = ⌊(T', fm')⌋" by(auto)
with hasf' have "P ⊢ D' ≼⇧* D" by(auto dest!: map_of_SomeD intro: has_fields_decl_above)
with classD DnObj have "(subcls1 P)^++ D D"
by(auto intro: subcls1.intros rtranclp_into_tranclp2)
with wf show False by(auto dest: subcls_irrefl)
qed
ultimately show ?thesis using FD hasf'
by(auto simp add: map_add_Some_iff intro: map_of_remap_conv simp del: map_map)
qed
with hasf show ?thesis unfolding sees_field_def by blast
qed
lemma has_fields_distinct:
assumes wf: "wf_prog wf_md P"
and "P ⊢ C has_fields FDTs"
shows "distinct (map fst FDTs)"
using ‹P ⊢ C has_fields FDTs›
proof(induct)
case (has_fields_Object D fs ms FDTs)
have eq: "map (fst ∘ (λ(F, y). ((F, Object), y))) fs = map ((λF. (F, Object)) ∘ fst) fs" by(auto)
from ‹class P Object = ⌊(D, fs, ms)⌋› wf
have "wf_cdecl wf_md P (Object, D, fs, ms)" by(rule class_wf)
hence "distinct (map fst fs)" by(simp add: wf_cdecl_def distinct_fst_def)
hence "distinct (map (fst ∘ (λ(F, y). ((F, Object), y))) fs)"
unfolding eq distinct_map by(auto intro: comp_inj_on inj_onI)
thus ?case using ‹FDTs = map (λ(F, T). ((F, Object), T)) fs› by(simp)
next
case (has_fields_rec C D fs ms FDTs FDTs')
have eq: "map (fst ∘ (λ(F, y). ((F, C), y))) fs = map ((λF. (F, C)) ∘ fst) fs" by(auto)
from ‹class P C = ⌊(D, fs, ms)⌋› wf
have "wf_cdecl wf_md P (C, D, fs, ms)" by(rule class_wf)
hence "distinct (map fst fs)" by(simp add: wf_cdecl_def distinct_fst_def)
hence "distinct (map (fst ∘ (λ(F, y). ((F, C), y))) fs)"
unfolding eq distinct_map by(auto intro: comp_inj_on inj_onI)
moreover from ‹class P C = ⌊(D, fs, ms)⌋› ‹C ≠ Object›
have "P ⊢ C ≺⇧1 D" by(rule subcls1.intros)
with ‹P ⊢ D has_fields FDTs›
have "(fst ∘ (λ(F, y). ((F, C), y))) ` set fs ∩ fst ` set FDTs = {}"
by(auto dest: subcls_notin_has_fields)
ultimately show ?case using ‹FDTs' = map (λ(F, T). ((F, C), T)) fs @ FDTs› ‹distinct (map fst FDTs)› by simp
qed
subsection ‹Code generation›
code_pred
(modes: i ⇒ i ⇒ i ⇒ bool)
[inductify]
wf_overriding
.
text ‹
Separate subclass acycilicity from class declaration check.
Otherwise, cyclic class hierarchies might lead to non-termination
as @{term "Methods"} recurses over the class hierarchy.
›
definition acyclic_class_hierarchy :: "'m prog ⇒ bool"
where
"acyclic_class_hierarchy P ⟷
(∀(C, D, fs, ml) ∈ set (classes P). C ≠ Object ⟶ ¬ P ⊢ D ≼⇧* C)"
definition wf_cdecl' :: "'m wf_mdecl_test ⇒ 'm prog ⇒ 'm cdecl ⇒ bool"
where
"wf_cdecl' wf_md P = (λ(C,(D,fs,ms)).
(∀f∈set fs. wf_fdecl P f) ∧ distinct_fst fs ∧
(∀m∈set ms. wf_mdecl wf_md P C m) ∧
distinct_fst ms ∧
(C ≠ Object ⟶ is_class P D ∧ (∀m∈set ms. wf_overriding P D m)) ∧
(C = Thread ⟶ (∃m. (run, [], Void, m) ∈ set ms)))"
lemma acyclic_class_hierarchy_code [code]:
"acyclic_class_hierarchy P ⟷ (∀(C, D, fs, ml) ∈ set (classes P). C ≠ Object ⟶ ¬ subcls' P D C)"
by(simp add: acyclic_class_hierarchy_def subcls'_def)
lemma wf_cdecl'_code [code]:
"wf_cdecl' wf_md P = (λ(C,(D,fs,ms)).
(∀f∈set fs. wf_fdecl P f) ∧ distinct_fst fs ∧
(∀m∈set ms. wf_mdecl wf_md P C m) ∧
distinct_fst ms ∧
(C ≠ Object ⟶ is_class P D ∧ (∀m∈set ms. wf_overriding P D m)) ∧
(C = Thread ⟶ ((run, [], Void) ∈ set (map (λ(M, Ts, T, b). (M, Ts, T)) ms))))"
by(auto simp add: wf_cdecl'_def intro!: ext intro: rev_image_eqI)
declare set_append [symmetric, code_unfold]
lemma wf_prog_code [code]:
"wf_prog wf_md P ⟷
acyclic_class_hierarchy P ∧
wf_syscls P ∧ distinct_fst (classes P) ∧
(∀c ∈ set (classes P). wf_cdecl' wf_md P c)"
unfolding wf_prog_def wf_cdecl_def wf_cdecl'_def acyclic_class_hierarchy_def split_def
by blast
end