Theory WellForm
section ‹ Generic Well-formedness of programs ›
theory WellForm imports TypeRel SystemClasses 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 @{text WellType}).
Because Jinja 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,b,T). is_type P T"
definition wf_mdecl :: "'m wf_mdecl_test ⇒ 'm wf_mdecl_test"
where
"wf_mdecl wf_md P C ≡ λ(M,b,Ts,T,m).
(∀T∈set Ts. is_type P T) ∧ is_type P T ∧ wf_md P C (M,b,Ts,T,m)"
definition wf_clinit :: "'m mdecl list ⇒ bool" where
"wf_clinit ms = (∃m. (clinit,Static,[],Void,m)∈set ms)"
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,b,Ts,T,m)∈set ms.
∀D' b' Ts' T' m'. P ⊢ D sees M,b':Ts' → T' = m' in D' ⟶
b = b' ∧ P ⊢ Ts' [≤] Ts ∧ P ⊢ T ≤ T')) ∧
wf_clinit ms"
definition wf_syscls :: "'m prog ⇒ bool"
where
"wf_syscls P ≡ {Object} ∪ sys_xcpts ⊆ set(map fst P)"
definition wf_prog :: "'m wf_mdecl_test ⇒ 'm prog ⇒ bool"
where
"wf_prog wf_md P ≡ wf_syscls P ∧ (∀c ∈ set P. wf_cdecl wf_md P c) ∧ distinct_fst P"
subsection‹ Well-formedness lemmas ›
lemma class_wf:
"⟦class P C = Some c; wf_prog wf_md P⟧ ⟹ wf_cdecl wf_md P (C,c)"
by (unfold wf_prog_def class_def) (fast dest: map_of_SomeD)
lemma class_Object [simp]:
"wf_prog wf_md P ⟹ ∃C fs ms. class P Object = Some (C,fs,ms)"
by (unfold wf_prog_def wf_syscls_def class_def)
(auto simp: map_of_SomeI)
lemma is_class_Object [simp]:
"wf_prog wf_md P ⟹ is_class P Object"
by (simp add: is_class_def)
lemma is_class_supclass:
assumes wf: "wf_prog wf_md P" and sub: "P ⊢ C ≼⇧* D"
shows "is_class P C ⟹ is_class P D"
using sub proof(induct)
case step then show ?case
by(auto simp:wf_cdecl_def is_class_def dest!:class_wf[OF _ wf] subcls1D)
qed simp
lemma is_class_xcpt:
"⟦ C ∈ sys_xcpts; wf_prog wf_md P ⟧ ⟹ is_class P C"
by (fastforce intro!: map_of_SomeI
simp add: wf_prog_def wf_syscls_def is_class_def class_def)
lemma subcls1_wfD:
assumes sub1: "P ⊢ C ≺⇧1 D" and wf: "wf_prog wf_md P"
shows "D ≠ C ∧ (D,C) ∉ (subcls1 P)⇧+"
proof -
obtain fs ms where "C ≠ Object" and cls: "class P C = ⌊(D, fs, ms)⌋"
using subcls1D[OF sub1] by clarify
then show ?thesis using wf class_wf[OF cls wf] r_into_trancl[OF sub1]
by(force simp add: wf_cdecl_def reflcl_trancl [THEN sym]
simp del: reflcl_trancl)
qed
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; (C,D) ∈ (subcls1 P)⇧+ ⟧ ⟹ (D,C) ∉ (subcls1 P)⇧+"
by(erule tranclE; fast dest!: subcls1_wfD intro: trancl_trans)
lemma subcls_irrefl:
"⟦ wf_prog wf_md P; (C,D) ∈ (subcls1 P)⇧+ ⟧ ⟹ C ≠ D"
by (erule trancl_trans_induct) (auto dest: subcls1_wfD subcls_asym)
lemma acyclic_subcls1:
"wf_prog wf_md P ⟹ acyclic (subcls1 P)"
by (unfold acyclic_def) (fast dest: subcls_irrefl)
lemma wf_subcls1:
"wf_prog wf_md P ⟹ wf ((subcls1 P)¯)"
proof -
assume wf: "wf_prog wf_md P"
have "finite (subcls1 P)" by(rule finite_subcls1)
then have fin': "finite ((subcls1 P)¯)" by(subst finite_converse)
from wf have "acyclic (subcls1 P)" by(rule acyclic_subcls1)
then have acyc': "acyclic ((subcls1 P)¯)" by (subst acyclic_converse)
from fin' acyc' show ?thesis by (rule finite_acyclic_wf)
qed
lemma single_valued_subcls1:
"wf_prog wf_md G ⟹ single_valued (subcls1 G)"
by(auto simp:wf_prog_def distinct_fst_def single_valued_def dest!:subcls1D)
lemma subcls_induct:
"⟦ wf_prog wf_md P; ⋀C. ∀D. (C,D) ∈ (subcls1 P)⇧+ ⟶ Q D ⟹ Q C ⟧ ⟹ Q C"
(is "?A ⟹ PROP ?P ⟹ _")
proof -
assume p: "PROP ?P"
assume ?A then have wf: "wf_prog wf_md P" by assumption
have wf':"wf (((subcls1 P)⇧+)¯)" using wf_trancl[OF wf_subcls1[OF wf]]
by(simp only: trancl_converse)
show ?thesis using wf_induct[where a = C and P = Q, OF wf' p] by simp
qed
lemma subcls1_induct_aux:
assumes "is_class P C" and wf: "wf_prog wf_md P" and QObj: "Q Object"
shows
"⟦ ⋀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 "PROP ?P ⟹ _")
proof -
assume p: "PROP ?P"
have "class P C ≠ None ⟶ Q C"
proof(induct rule: subcls_induct[OF wf])
case (1 C)
have "class P C ≠ None ⟹ Q C"
proof(cases "C = Object")
case True
then show ?thesis using QObj by fast
next
case False
assume nNone: "class P C ≠ None"
then have is_cls: "is_class P C" by(simp add: is_class_def)
obtain D fs ms where cls: "class P C = ⌊(D, fs, ms)⌋" using nNone by safe
also have wfC: "wf_cdecl wf_md P (C, D, fs, ms)" by(rule class_wf[OF cls wf])
moreover have D: "is_class P D" by(rule wf_cdecl_supD[OF wfC False])
moreover have "P ⊢ C ≺⇧1 D" by(rule subcls1I[OF cls False])
moreover have "class P D ≠ None" using D by(simp add: is_class_def)
ultimately show ?thesis using 1 by (auto intro: p[OF False is_cls])
qed
then show "class P C ≠ None ⟶ Q C" by simp
qed
thus ?thesis using assms by(unfold is_class_def) simp
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"
by (erule (2) subcls1_induct_aux) blast
lemma subcls_C_Object:
assumes "class": "is_class P C" and wf: "wf_prog wf_md P"
shows "P ⊢ C ≼⇧* Object"
using wf "class"
proof(induct rule: subcls1_induct)
case Subcls
then show ?case by(simp add: converse_rtrancl_into_rtrancl)
qed fast
lemma is_type_pTs:
assumes "wf_prog wf_md P" and "(C,S,fs,ms) ∈ set P" and "(M,b,Ts,T,m) ∈ set ms"
shows "set Ts ⊆ types P"
proof
from assms have "wf_mdecl wf_md P C (M,b,Ts,T,m)"
by (unfold wf_prog_def wf_cdecl_def) auto
hence "∀t ∈ set Ts. is_type P t" by (unfold wf_mdecl_def) auto
moreover fix t assume "t ∈ set Ts"
ultimately have "is_type P t" by blast
thus "t ∈ types P" ..
qed
lemma wf_supercls_distinct_app:
assumes wf:"wf_prog wf_md P"
and nObj: "C ≠ Object" and cls: "class P C = ⌊(D, fs, ms)⌋"
and super: "supercls_lst P (C#Cs)" and dist: "distinct (C#Cs)"
shows "distinct (D#C#Cs)"
proof -
have "¬ P ⊢ D ≼⇧* C" using subcls1_wfD[OF subcls1I[OF cls nObj] wf]
by (simp add: rtrancl_eq_or_trancl)
then show ?thesis using assms by auto
qed
subsection‹ Well-formedness and method lookup ›
lemma sees_wf_mdecl:
assumes wf: "wf_prog wf_md P" and sees: "P ⊢ C sees M,b:Ts→T = m in D"
shows "wf_mdecl wf_md P D (M,b,Ts,T,m)"
using wf visible_method_exists[OF sees] proof(cases b)
qed (fastforce simp:wf_cdecl_def dest!:class_wf dest:map_of_SomeD)+
lemma sees_method_mono [rule_format (no_asm)]:
assumes sub: "P ⊢ C' ≼⇧* C" and wf: "wf_prog wf_md P"
shows "∀D b Ts T m. P ⊢ C sees M,b:Ts→T = m in D ⟶
(∃D' Ts' T' m'. P ⊢ C' sees M,b:Ts'→T' = m' in D' ∧ P ⊢ Ts [≤] Ts' ∧ P ⊢ T' ≤ T)"
(is "∀D b Ts T m. ?P C D b Ts T m ⟶ ?Q C' D b Ts T m")
proof(rule disjE[OF rtranclD[OF sub]])
assume "C' = C"
then show ?thesis using assms by fastforce
next
assume "C' ≠ C ∧ (C', C) ∈ (subcls1 P)⇧+"
then have neq: "C' ≠ C" and subcls1: "(C', C) ∈ (subcls1 P)⇧+" by simp+
show ?thesis proof(induct rule: trancl_trans_induct[OF subcls1])
case (2 x y z)
then have zy: "⋀D b Ts T m. ?P z D b Ts T m ⟹ ?Q y D b Ts T m" by blast
have "⋀D b Ts T m. ?P z D b Ts T m ⟹ ?Q x D b Ts T m"
proof -
fix D b Ts T m assume P: "?P z D b Ts T m"
then show "?Q x D b Ts T m" using zy[OF P] 2(2)
by(fast elim: widen_trans widens_trans)
qed
then show ?case by blast
next
case (1 x y)
have "⋀D b Ts T m. ?P y D b Ts T m ⟹ ?Q x D b Ts T m"
proof -
fix D b Ts T m assume P: "?P y D b Ts T m"
then obtain Mm where sees: "P ⊢ y sees_methods Mm" and
M: "Mm M = ⌊((b, Ts, T, m), D)⌋"
by(clarsimp simp:Method_def)
obtain fs ms where nObj: "x ≠ Object" and
cls: "class P x = ⌊(y, fs, ms)⌋"
using subcls1D[OF 1] by clarsimp
have x_meth: "P ⊢ x sees_methods Mm ++ (map_option (λm. (m, x)) ∘ map_of ms)"
using sees_methods_rec[OF cls nObj sees] by simp
show "?Q x D b Ts T m" proof(cases "map_of ms M")
case None
then have "∃m'. P ⊢ x sees M, b : Ts→T = m' in D" using M x_meth
by(fastforce simp add:Method_def map_add_def split:option.split)
then show ?thesis by auto
next
case (Some a)
then obtain b' Ts' T' m' where a: "a = (b',Ts',T',m')" by(cases a)
then have "(∃m' Mm. P ⊢ y sees_methods Mm ∧ Mm M = ⌊((b, Ts, T, m'), D)⌋)
⟶ b' = b ∧ P ⊢ Ts [≤] Ts' ∧ P ⊢ T' ≤ T"
using nObj class_wf[OF cls wf] map_of_SomeD[OF Some]
by(clarsimp simp: wf_cdecl_def Method_def) fast
then show ?thesis using Some a sees M x_meth
by(fastforce simp:Method_def map_add_def split:option.split)
qed
qed
then show ?case by simp
qed
qed
lemma sees_method_mono2:
"⟦ P ⊢ C' ≼⇧* C; wf_prog wf_md P;
P ⊢ C sees M,b:Ts→T = m in D; P ⊢ C' sees M,b':Ts'→T' = m' in D' ⟧
⟹ b = b' ∧ 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,b,Ts,T,m) ∈ set ms. Mm M = Some((b,Ts,T,m),C))"
using wf "class"
proof (induct rule:subcls1_induct)
case Object
with wf have dfst:"distinct_fst ms"
by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
with dfst have "distinct_fst ms"
by(blast dest: distinct_fst_appendD)
with Object show ?case by(fastforce intro!: sees_methods_Object map_of_SomeI)
next
case Subcls
with wf have dfst:"distinct_fst ms"
by (unfold class_def wf_prog_def wf_cdecl_def) (fastforce dest:map_of_SomeD)
with dfst have "distinct_fst ms"
by(blast dest: distinct_fst_appendD)
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: "(C,S,fs,ms) ∈ set P" and m: "(M,b,Ts,T,m) ∈ set ms"
shows "P ⊢ C sees M,b:Ts→T = m in C"
proof -
from wf C have "class": "class P C = Some (S,fs,ms)"
by (auto simp add: wf_prog_def class_def is_class_def intro: map_of_SomeI)
from "class" have "is_class P C" by(auto simp:is_class_def)
with assms "class" show ?thesis
by(bestsimp simp:Method_def dest:mdecls_visible)
qed
lemma Call_lemma:
assumes sees: "P ⊢ C sees M,b:Ts→T = m in D" and sub: "P ⊢ C' ≼⇧* C" and wf: "wf_prog wf_md P"
shows "∃D' Ts' T' m'.
P ⊢ C' sees M,b: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) ∧ wf_md P D' (M,b,Ts',T',m')"
using assms sees_method_mono[OF sub wf sees]
by(fastforce intro:sees_method_decl_above dest:sees_wf_mdecl
simp: wf_mdecl_def)
lemma wf_prog_lift:
assumes wf: "wf_prog (λP C bd. A P C bd) P"
and rule:
"⋀wf_md C M b Ts C T m bd.
wf_prog wf_md P ⟹
P ⊢ C sees M,b:Ts→T = m in C ⟹
set Ts ⊆ types P ⟹
bd = (M,b,Ts,T,m) ⟹
A P C bd ⟹
B P C bd"
shows "wf_prog (λP C bd. B P C bd) P"
proof -
have "⋀c. c∈set P ⟹ wf_cdecl A P c ⟹ wf_cdecl B P c"
proof -
fix c assume "c∈set P" and "wf_cdecl A P c"
then show "wf_cdecl B P c"
using rule[OF wf mdecl_visible[OF wf] is_type_pTs[OF wf]]
by (auto simp: wf_cdecl_def wf_mdecl_def)
qed
then show ?thesis using wf by (clarsimp simp: wf_prog_def)
qed
lemma wf_sees_clinit:
assumes wf:"wf_prog wf_md P" and ex: "class P C = Some a"
shows "∃m. P ⊢ C sees clinit,Static:[] → Void = m in C"
proof -
from ex obtain D fs ms where "a = (D,fs,ms)" by(cases a)
then have sP: "(C, D, fs, ms) ∈ set P" using ex map_of_SomeD[of P C a] by(simp add: class_def)
then have "wf_clinit ms" using assms by(unfold wf_prog_def wf_cdecl_def, auto)
then obtain m where sm: "(clinit, Static, [], Void, m) ∈ set ms" by (meson wf_clinit_def)
then have "P ⊢ C sees clinit,Static:[] → Void = m in C"
using mdecl_visible[OF wf sP sm] by simp
then show ?thesis by(rule exI)
qed
lemma wf_sees_clinit1:
assumes wf:"wf_prog wf_md P" and ex: "class P C = Some a"
and "P ⊢ C sees clinit,b:Ts → T = m in D"
shows "b = Static ∧ Ts = [] ∧ T = Void ∧ D = C"
proof -
obtain m' where sees: "P ⊢ C sees clinit,Static:[] → Void = m' in C"
using wf_sees_clinit[OF wf ex] by clarify
then show ?thesis using sees wf by (meson assms(3) sees_method_fun)
qed
lemma wf_NonStatic_nclinit:
assumes wf: "wf_prog wf_md P" and meth: "P ⊢ C sees M,NonStatic:Ts→T=(mxs,mxl,ins,xt) in D"
shows "M ≠ clinit"
proof -
from sees_method_is_class[OF meth] obtain a where cls: "class P C = Some a"
by(clarsimp simp: is_class_def)
with wf wf_sees_clinit[OF wf cls]
obtain m where "P ⊢ C sees clinit,Static:[]→Void=m in C" by clarsimp
with meth show ?thesis by(auto dest: sees_method_fun)
qed
subsection‹ Well-formedness and field lookup ›
lemma wf_Fields_Ex:
assumes wf: "wf_prog wf_md P" and "is_class P C"
shows "∃FDTs. P ⊢ C has_fields FDTs"
using assms proof(induct rule:subcls1_induct)
case Object
then show ?case using class_Object[OF wf]
by(blast intro:has_fields_Object)
next
case Subcls
then show ?case by(blast intro:has_fields_rec dest:subcls1D)
qed
lemma has_fields_types:
"⟦ P ⊢ C has_fields FDTs; (FD,b,T) ∈ set FDTs; wf_prog wf_md P ⟧ ⟹ is_type P T"
proof(induct rule:Fields.induct)
qed(fastforce dest!: class_wf simp: wf_cdecl_def wf_fdecl_def)+
lemma sees_field_is_type:
"⟦ P ⊢ C sees F,b:T in D; wf_prog wf_md P ⟧ ⟹ is_type P T"
by (meson has_field_def has_fields_types has_visible_field map_of_SomeD)
lemma wf_syscls:
"set SystemClasses ⊆ set P ⟹ wf_syscls P"
by (force simp: image_def SystemClasses_def wf_syscls_def sys_xcpts_def
ObjectC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def
NoClassDefFoundC_def
IncompatibleClassChangeC_def NoSuchFieldC_def NoSuchMethodC_def)
subsection‹ Well-formedness and subclassing ›
lemma wf_subcls_nCls:
assumes wf: "wf_prog wf_md P" and ns: "¬ is_class P C"
shows "⟦ P ⊢ D ≼⇧* D'; D ≠ C ⟧ ⟹ D' ≠ C"
proof(induct rule: rtrancl.induct)
case (rtrancl_into_rtrancl a b c)
with ns show ?case by(clarsimp dest!: subcls1D wf_cdecl_supD[OF class_wf[OF _ wf]])
qed(simp)
lemma wf_subcls_nCls':
assumes wf: "wf_prog wf_md P" and ns: "¬is_class P C⇩0"
shows "⋀cd D'. cd ∈ set P ⟹ ¬P ⊢ fst cd ≼⇧* C⇩0"
proof -
fix cd D' assume cd: "cd ∈ set P"
then have cls: "is_class P (fst cd)" using class_exists_equiv is_class_def by blast
with wf_subcls_nCls[OF wf ns] ns show "¬P ⊢ fst cd ≼⇧* C⇩0" by(cases "fst cd = D'", auto)
qed
lemma wf_nclass_nsub:
"⟦ wf_prog wf_md P; is_class P C; ¬is_class P C' ⟧ ⟹ ¬P ⊢ C ≼⇧* C'"
by(rule notI, auto dest: wf_subcls_nCls[where C=C' and D=C])
lemma wf_sys_xcpt_nsub_Start:
assumes wf: "wf_prog wf_md P" and ns: "¬is_class P Start" and sx: "C ∈ sys_xcpts"
shows "¬P ⊢ C ≼⇧* Start"
proof -
have Cns: "C ≠ Start" using Start_nsys_xcpts sx by clarsimp
show ?thesis using wf_subcls_nCls[OF wf ns _ Cns] by auto
qed
end