Theory StoreProperties
section ‹Store Properties›
theory StoreProperties
imports Store
begin
text ‹This theory formalizes advanced concepts and properties of stores.›
subsection ‹Reachability of a Location from a Reference›
text ‹For a given store, the function ‹reachS› yields the set of all pairs
$(l,v)$ where $l$ is a location that is reachable from the value $v$ (which must be a reference)
in the given store.
The predicate ‹reach› decides whether a location is reachable from a value in a store.
›
inductive
reach :: "Store ⇒ Location ⇒ Value ⇒ bool"
("_⊢ _ reachable'_from _" [91,91,91]90)
for s :: Store
where
Immediate: "ref l ≠ nullV ⟹ s⊢ l reachable_from (ref l)"
| Indirect: "⟦s⊢ l reachable_from (s@@k); ref k ≠ nullV⟧
⟹ s⊢ l reachable_from (ref k)"
text ‹Note that we explicitly exclude ‹nullV› as legal reference
for reachability.
Keep in mind that static fields are not associated to any object,
therefore ‹ref› yields ‹nullV› if invoked on static fields
(see the
definition of the function ‹ref›, Sect. \ref{ref_def}).
Reachability only describes the locations directly
reachable from the object or array by following the pointers and should not include
the static fields if we encounter a ‹nullV› reference in the pointer
chain.›
text ‹We formalize some properties of reachability.
Especially, Lemma 3.2 as given in \<^cite>‹‹p. 53› in "Poetzsch-Heffter97specification"› is proven.›
lemma unreachable_Null:
assumes reach: "s⊢ l reachable_from x" shows "x≠nullV"
using reach by (induct) auto
corollary unreachable_Null_simp [simp]:
"¬ s⊢ l reachable_from nullV"
by (iprover dest: unreachable_Null)
corollary unreachable_NullE [elim]:
"s⊢ l reachable_from nullV ⟹ P"
by (simp)
lemma reachObjLoc [simp,intro]:
"C=cls cf ⟹ s⊢ objLoc cf a reachable_from objV C a"
by (iprover intro: reach.Immediate [of "objLoc cf a",simplified])
lemma reachArrLoc [simp,intro]: "s⊢ arrLoc T a i reachable_from arrV T a"
by (rule reach.Immediate [of "arrLoc T a i",simplified])
lemma reachArrLen [simp,intro]: "s⊢ arrLenLoc T a reachable_from arrV T a"
by (rule reach.Immediate [of "arrLenLoc T a",simplified])
lemma unreachStatic [simp]: "¬ s⊢ staticLoc f reachable_from x"
proof -
{
fix y assume "s⊢ y reachable_from x" "y=staticLoc f"
then have False
by induct auto
}
thus ?thesis
by auto
qed
lemma unreachStaticE [elim]: "s⊢ staticLoc f reachable_from x ⟹ P"
by (simp add: unreachStatic)
lemma reachable_from_ArrLoc_impl_Arr [simp,intro]:
assumes reach_loc: "s⊢ l reachable_from (s@@arrLoc T a i)"
shows "s⊢ l reachable_from (arrV T a)"
using reach.Indirect [OF reach_loc]
by simp
lemma reachable_from_ObjLoc_impl_Obj [simp,intro]:
assumes reach_loc: "s⊢ l reachable_from (s@@objLoc cf a)"
assumes C: "C=cls cf"
shows "s⊢ l reachable_from (objV C a)"
using C reach.Indirect [OF reach_loc]
by simp
text ‹Lemma 3.2 (i)›
lemma reach_update [simp]:
assumes unreachable_l_x: "¬ s⊢ l reachable_from x"
shows "s⟨l:=y⟩⊢ k reachable_from x = s⊢ k reachable_from x"
proof
assume "s⊢ k reachable_from x"
from this unreachable_l_x
show "s⟨l := y⟩⊢ k reachable_from x"
proof (induct)
case (Immediate k)
have "ref k ≠ nullV" by fact
then show "s⟨l := y⟩⊢ k reachable_from (ref k)"
by (rule reach.Immediate)
next
case (Indirect k m)
have hyp: "¬ s⊢ l reachable_from (s@@m)
⟹ s⟨l:=y⟩ ⊢ k reachable_from (s@@m)" by fact
have "ref m ≠ nullV" and "¬ s⊢ l reachable_from (ref m)" by fact+
hence "l≠m" "¬ s⊢ l reachable_from (s@@m)"
by (auto intro: reach.intros)
with hyp have "s⟨l := y⟩ ⊢ k reachable_from (s⟨l := y⟩@@m)"
by simp
then show "s⟨l := y⟩⊢ k reachable_from (ref m)"
by (rule reach.Indirect) (rule Indirect.hyps)
qed
next
assume "s⟨l := y⟩⊢ k reachable_from x"
from this unreachable_l_x
show "s⊢ k reachable_from x"
proof (induct)
case (Immediate k)
have "ref k ≠ nullV" by fact
then show "s ⊢ k reachable_from (ref k)"
by (rule reach.Immediate)
next
case (Indirect k m)
with Indirect.hyps
have hyp: "¬ s⊢ l reachable_from (s⟨l := y⟩@@m)
⟹ s⊢ k reachable_from (s⟨l := y⟩@@m)" by simp
have "ref m ≠ nullV" and "¬ s⊢ l reachable_from (ref m)" by fact+
hence "l≠m" "¬ s ⊢ l reachable_from (s@@m)"
by (auto intro: reach.intros)
with hyp have "s ⊢ k reachable_from (s@@m)"
by simp
thus "s⊢ k reachable_from (ref m)"
by (rule reach.Indirect) (rule Indirect.hyps)
qed
qed
text ‹Lemma 3.2 (ii)›
lemma reach2:
"¬ s⊢ l reachable_from x ⟹ ¬ s⟨l:=y⟩⊢ l reachable_from x"
by (simp)
text ‹Lemma 3.2 (iv)›
lemma reach4: "¬ s ⊢ l reachable_from (ref k) ⟹ k ≠ l ∨ (ref k) = nullV"
by (auto intro: reach.intros)
lemma reachable_isRef:
assumes reach: "s⊢l reachable_from x"
shows "isRefV x"
using reach
proof (induct)
case (Immediate l)
show "isRefV (ref l)"
by (cases l) simp_all
next
case (Indirect l k)
show "isRefV (ref k)"
by (cases k) simp_all
qed
lemma val_ArrLen_IntgT: "isArrLenLoc l ⟹ typeof (s@@l) = IntgT"
proof -
assume isArrLen: "isArrLenLoc l"
have T: "typeof (s@@l) ≤ ltype l"
by (simp)
also from isArrLen have I: "ltype l = IntgT"
by (cases l) simp_all
finally show ?thesis
by (auto elim: rtranclE simp add: le_Javatype_def subtype_defs)
qed
lemma access_alloc' [simp]:
assumes no_arr_len: "¬ isArrLenLoc l"
shows "s⟨t⟩@@l = s@@l"
proof -
from no_arr_len
have "isNewArr t ⟶ l ≠ arr_len (new s t)"
by (cases t) (auto simp add: new_def isArrLenLoc_def split: Location.splits)
thus ?thesis
by (rule access_alloc)
qed
text ‹Lemma 3.2 (v)›
lemma reach_alloc [simp]: "s⟨t⟩⊢ l reachable_from x = s⊢ l reachable_from x"
proof
assume "s⟨t⟩⊢ l reachable_from x"
thus "s⊢ l reachable_from x"
proof (induct)
case (Immediate l)
thus "s⊢ l reachable_from ref l"
by (rule reach.intros)
next
case (Indirect l k)
have reach_k: "s⊢ l reachable_from (s⟨t⟩@@k)" by fact
moreover
have "s⟨t⟩@@k = s@@k"
proof -
from reach_k have isRef: "isRefV (s⟨t⟩@@k)"
by (rule reachable_isRef)
have "¬ isArrLenLoc k"
proof (rule ccontr,simp)
assume "isArrLenLoc k"
then have "typeof (s⟨t⟩@@k) = IntgT"
by (rule val_ArrLen_IntgT)
with isRef
show "False"
by (cases "(s⟨t⟩@@k)") simp_all
qed
thus ?thesis
by (rule access_alloc')
qed
ultimately have "s⊢ l reachable_from (s@@k)"
by simp
thus "s⊢ l reachable_from ref k"
by (rule reach.intros) (rule Indirect.hyps)
qed
next
assume "s⊢ l reachable_from x"
thus "s⟨t⟩⊢ l reachable_from x"
proof (induct)
case (Immediate l)
thus "s⟨t⟩⊢ l reachable_from ref l"
by (rule reach.intros)
next
case (Indirect l k)
have reach_k: "s⟨t⟩⊢ l reachable_from (s@@k)" by fact
moreover
have "s⟨t⟩@@k = s@@k"
proof -
from reach_k have isRef: "isRefV (s@@k)"
by (rule reachable_isRef)
have "¬ isArrLenLoc k"
proof (rule ccontr,simp)
assume "isArrLenLoc k"
then have "typeof (s@@k) = IntgT"
by (rule val_ArrLen_IntgT)
with isRef
show "False"
by (cases "(s@@k)") simp_all
qed
thus ?thesis
by (rule access_alloc')
qed
ultimately have "s⟨t⟩⊢ l reachable_from (s⟨t⟩@@k)"
by simp
thus "s⟨t⟩⊢ l reachable_from ref k"
by (rule reach.intros) (rule Indirect.hyps)
qed
qed
text ‹Lemma 3.2 (vi)›
lemma reach6: "isprimitive(typeof x) ⟹ ¬ s ⊢ l reachable_from x"
proof
assume prim: "isprimitive(typeof x)"
assume "s ⊢ l reachable_from x"
hence "isRefV x"
by (rule reachable_isRef)
with prim show False
by (cases x) simp_all
qed
text ‹Lemma 3.2 (iii)›
lemma reach3:
assumes k_y: "¬ s⊢ k reachable_from y"
assumes k_x: "¬ s⊢ k reachable_from x"
shows "¬ s⟨l:=y⟩⊢ k reachable_from x"
proof
assume "s⟨l:=y⟩⊢ k reachable_from x"
from this k_y k_x
show False
proof (induct)
case (Immediate l)
have "¬ s⊢ l reachable_from ref l" and "ref l ≠ nullV" by fact+
thus False
by (iprover intro: reach.intros)
next
case (Indirect m k)
have k_not_Null: "ref k ≠ nullV" by fact
have not_m_y: "¬ s⊢ m reachable_from y" by fact
have not_m_k: "¬ s⊢ m reachable_from ref k" by fact
have hyp: "⟦¬ s⊢ m reachable_from y; ¬ s⊢ m reachable_from (s⟨l := y⟩@@k)⟧
⟹ False" by fact
have m_upd_k: "s⟨l := y⟩⊢ m reachable_from (s⟨l := y⟩@@k)" by fact
show False
proof (cases "l=k")
case False
then have "s⟨l := y⟩@@k = s@@k" by simp
moreover
from not_m_k k_not_Null have "¬ s⊢ m reachable_from (s@@k)"
by (iprover intro: reach.intros)
ultimately show False
using not_m_y hyp by simp
next
case True note eq_l_k = this
show ?thesis
proof (cases "alive (ref l) s ∧ alive y s ∧ typeof y ≤ ltype l")
case True
with eq_l_k have "s⟨l := y⟩@@k = y"
by simp
with not_m_y hyp show False by simp
next
case False
hence "s⟨l := y⟩ = s"
by auto
moreover
from not_m_k k_not_Null have "¬ s⊢ m reachable_from (s@@k)"
by (iprover intro: reach.intros)
ultimately show False
using not_m_y hyp by simp
qed
qed
qed
qed
text ‹Lemma 3.2 (vii).›
lemma unreachable_from_init [simp,intro]: "¬ s⊢ l reachable_from (init T)"
using reach6 by (cases T) simp_all
lemma ref_reach_unalive:
assumes unalive_x:"¬ alive x s"
assumes l_x: "s⊢ l reachable_from x"
shows "x = ref l"
using l_x unalive_x
proof induct
case (Immediate l)
show "ref l = ref l"
by simp
next
case (Indirect l k)
have "ref k ≠ nullV" by fact
have "¬ alive (ref k) s" by fact
hence "s@@k = init (ltype k)" by simp
moreover have "s⊢ l reachable_from (s@@k)" by fact
ultimately have False by simp
thus ?case ..
qed
lemma loc_new_reach:
assumes l: "ref l = new s t"
assumes l_x: "s⊢ l reachable_from x"
shows "x = new s t"
using l_x l
proof induct
case (Immediate l)
show "ref l = new s t" by fact
next
case (Indirect l k)
hence "s@@k = new s t" by iprover
moreover
have "¬ alive (new s t) s"
by simp
moreover
have "alive (s@@k) s"
by simp
ultimately have False by simp
thus ?case ..
qed
text ‹Lemma 3.2 (viii)›
lemma alive_reach_alive:
assumes alive_x: "alive x s"
assumes reach_l: "s ⊢ l reachable_from x"
shows "alive (ref l) s"
using reach_l alive_x
proof (induct)
case (Immediate l)
show ?case by fact
next
case (Indirect l k)
have hyp: "alive (s@@k) s ⟹ alive (ref l) s" by fact
moreover have "alive (s@@k) s" by simp
ultimately
show "alive (ref l) s"
by iprover
qed
text ‹Lemma 3.2 (ix)›
lemma reach9:
assumes reach_impl_access_eq: "∀l. s1⊢l reachable_from x ⟶ (s1@@l = s2@@l)"
shows "s1⊢ l reachable_from x = s2⊢ l reachable_from x"
proof
assume "s1⊢ l reachable_from x"
from this reach_impl_access_eq
show "s2⊢ l reachable_from x"
proof (induct)
case (Immediate l)
show "s2⊢ l reachable_from ref l"
by (rule reach.intros) (rule Immediate.hyps)
next
case (Indirect l k)
have hyp: "∀l. s1⊢ l reachable_from (s1@@k) ⟶ s1@@l = s2@@l
⟹ s2⊢ l reachable_from (s1@@k)" by fact
have k_not_Null: "ref k ≠ nullV" by fact
have reach_impl_access_eq:
"∀l. s1⊢ l reachable_from ref k ⟶ s1@@l = s2@@l" by fact
have "s1⊢ l reachable_from (s1@@k)" by fact
with k_not_Null
have "s1@@k = s2@@k"
by (iprover intro: reach_impl_access_eq [rule_format] reach.intros)
moreover from reach_impl_access_eq k_not_Null
have "∀l. s1⊢ l reachable_from (s1@@k) ⟶ s1@@l = s2@@l"
by (iprover intro: reach.intros)
then have "s2⊢ l reachable_from (s1@@k)"
by (rule hyp)
ultimately have "s2⊢ l reachable_from (s2@@k)"
by simp
thus "s2⊢ l reachable_from ref k"
by (rule reach.intros) (rule Indirect.hyps)
qed
next
assume "s2⊢ l reachable_from x"
from this reach_impl_access_eq
show "s1⊢ l reachable_from x"
proof (induct)
case (Immediate l)
show "s1⊢ l reachable_from ref l"
by (rule reach.intros) (rule Immediate.hyps)
next
case (Indirect l k)
have hyp: "∀l. s1⊢ l reachable_from (s2@@k) ⟶ s1@@l = s2@@l
⟹ s1⊢ l reachable_from (s2@@k)" by fact
have k_not_Null: "ref k ≠ nullV" by fact
have reach_impl_access_eq:
"∀l. s1⊢ l reachable_from ref k ⟶ s1@@l = s2@@l" by fact
have "s1⊢ k reachable_from ref k"
by (rule reach.intros) (rule Indirect.hyps)
with reach_impl_access_eq
have eq_k: "s1@@k = s2@@k"
by simp
from reach_impl_access_eq k_not_Null
have "∀l. s1⊢ l reachable_from (s1@@k) ⟶ s1@@l = s2@@l"
by (iprover intro: reach.intros)
then
have "∀l. s1⊢ l reachable_from (s2@@k) ⟶ s1@@l = s2@@l"
by (simp add: eq_k)
with eq_k hyp have "s1⊢ l reachable_from (s1@@k)"
by simp
thus "s1⊢ l reachable_from ref k"
by (rule reach.intros) (rule Indirect.hyps)
qed
qed
subsection ‹Reachability of a Reference from a Reference›
text ‹The predicate ‹rreach› tests whether a value is reachable from
another value. This is an extension of the predicate ‹oreach› as described
in \<^cite>‹‹p. 54› in "Poetzsch-Heffter97specification"› because now arrays are handled as well.
›
definition rreach:: "Store ⇒ Value ⇒ Value ⇒ bool"
("_⊢Ref _ reachable'_from _" [91,91,91]90) where
"s⊢Ref y reachable_from x = (∃ l. s⊢ l reachable_from x ∧ y = ref l)"
subsection ‹Disjointness of Reachable Locations›
text ‹The predicate ‹disj› tests whether two values are disjoint
in a given store. Its properties as given in
\<^cite>‹‹Lemma 3.3, p. 54› in "Poetzsch-Heffter97specification"› are then proven.
›
definition disj:: "Value ⇒ Value ⇒ Store ⇒ bool" where
"disj x y s = (∀ l. ¬ s⊢ l reachable_from x ∨ ¬ s⊢ l reachable_from y)"
lemma disjI1: "⟦⋀ l. s⊢ l reachable_from x ⟹ ¬ s⊢ l reachable_from y⟧
⟹ disj x y s"
by (simp add: disj_def)
lemma disjI2: "⟦⋀ l. s⊢ l reachable_from y ⟹ ¬ s⊢ l reachable_from x⟧
⟹ disj x y s"
by (auto simp add: disj_def)
lemma disj_cases [consumes 1]:
assumes "disj x y s"
assumes "⋀ l. ¬ s⊢ l reachable_from x ⟹ P"
assumes "⋀ l. ¬ s⊢ l reachable_from y ⟹ P"
shows "P"
using assms by (auto simp add: disj_def)
text ‹Lemma 3.3 (i) in \<^cite>‹"Poetzsch-Heffter97specification"››
lemma disj1: "⟦disj x y s; ¬ s⊢ l reachable_from x; ¬ s⊢ l reachable_from y⟧
⟹ disj x y (s⟨l:=z⟩)"
by (auto simp add: disj_def)
text ‹Lemma 3.3 (ii)›
lemma disj2:
assumes disj_x_y: "disj x y s"
assumes disj_x_z: "disj x z s"
assumes unreach_l_x: "¬ s⊢ l reachable_from x"
shows "disj x y (s⟨l:=z⟩)"
proof (rule disjI1)
fix k
assume reach_k_x: "s⟨l := z⟩⊢ k reachable_from x"
show "¬ s⟨l := z⟩⊢ k reachable_from y"
proof -
from unreach_l_x reach_k_x
have reach_s_k_x: "s⊢ k reachable_from x"
by simp
with disj_x_z
have "¬ s⊢ k reachable_from z"
by (simp add: disj_def)
moreover from reach_s_k_x disj_x_y
have "¬ s⊢ k reachable_from y"
by (simp add: disj_def)
ultimately show ?thesis
by (rule reach3)
qed
qed
text ‹Lemma 3.3 (iii)›
lemma disj3: assumes alive_x_s: "alive x s"
shows "disj x (new s t) (s⟨t⟩)"
proof (rule disjI1,simp only: reach_alloc)
fix l
assume reach_l_x: "s⊢ l reachable_from x"
show "¬ s⊢ l reachable_from new s t"
proof
assume reach_l_new: "s⊢ l reachable_from new s t"
have unalive_new: "¬ alive (new s t) s" by simp
from this reach_l_new
have "new s t = ref l"
by (rule ref_reach_unalive)
moreover from alive_x_s reach_l_x
have "alive (ref l) s"
by (rule alive_reach_alive)
ultimately show False
using unalive_new
by simp
qed
qed
text ‹Lemma 3.3 (iv)›
lemma disj4: "⟦disj (objV C a) y s; CClassT C ≤ dtype f ⟧
⟹ disj (s@@(objV C a)..f) y s"
by (auto simp add: disj_def)
lemma disj4': "⟦disj (arrV T a) y s ⟧
⟹ disj (s@@(arrV T a).[i]) y s"
by (auto simp add: disj_def)
subsection ‹X-Equivalence›
text ‹We call two stores $s_1$ and $s_2$ equivalent wrt. a given value $X$
(which is called X-equivalence)
iff $X$ and all values
reachable from $X$ in $s_1$ or $s_2$ have the same state \<^cite>‹‹p. 55› in "Poetzsch-Heffter97specification"›.
This is tested by the predicate
‹xeq›. Lemma 3.4 of \<^cite>‹"Poetzsch-Heffter97specification"› is then proven for ‹xeq›.
›
definition xeq:: "Value ⇒ Store ⇒ Store ⇒ bool" where
"xeq x s t = (alive x s = alive x t ∧
(∀ l. s⊢ l reachable_from x ⟶ s@@l = t@@l))"
abbreviation xeq_syntax :: "Store ⇒ Value ⇒ Store ⇒ bool"
("_/ (≡[_])/ _" [900,0,900] 900)
where "s ≡[x] t == xeq x s t"
lemma xeqI: "⟦alive x s = alive x t;
⋀ l. s⊢ l reachable_from x ⟹ s@@l = t@@l
⟧ ⟹ s ≡[x] t"
by (auto simp add: xeq_def)
text ‹Lemma 3.4 (i) in \<^cite>‹"Poetzsch-Heffter97specification"›.›
lemma xeq1_refl: "s ≡[x] s"
by (simp add: xeq_def)
text ‹Lemma 3.4 (i)›
lemma xeq1_sym':
assumes s_t: "s ≡[x] t"
shows "t ≡[x] s"
proof -
from s_t have "alive x s = alive x t" by (simp add: xeq_def)
moreover
from s_t have "∀ l. s⊢ l reachable_from x ⟶ s@@l = t@@l"
by (simp add: xeq_def)
with reach9 [OF this]
have "∀ l. t⊢ l reachable_from x ⟶ t@@l = s@@l"
by simp
ultimately show ?thesis
by (simp add: xeq_def)
qed
lemma xeq1_sym: "s ≡[x] t = t ≡[x] s"
by (auto intro: xeq1_sym')
text ‹Lemma 3.4 (i)›
lemma xeq1_trans [trans]:
assumes s_t: "s ≡[x] t"
assumes t_r: "t ≡[x] r"
shows "s ≡[x] r"
proof -
from s_t t_r
have "alive x s = alive x r"
by (simp add: xeq_def)
moreover
have "∀ l. s⊢ l reachable_from x ⟶ s@@l = r@@l"
proof (intro allI impI)
fix l
assume reach_l: "s⊢ l reachable_from x"
show "s@@l = r@@l"
proof -
from reach_l s_t have "s@@l=t@@l"
by (simp add: xeq_def)
also have "t@@l = r@@l"
proof -
from s_t have "∀ l. s⊢ l reachable_from x ⟶ s@@l = t@@l"
by (simp add: xeq_def)
from reach9 [OF this] reach_l have "t⊢ l reachable_from x"
by simp
with t_r show ?thesis
by (simp add: xeq_def)
qed
finally show ?thesis .
qed
qed
ultimately show ?thesis
by (simp add: xeq_def)
qed
text ‹Lemma 3.4 (ii)›
lemma xeq2:
assumes xeq: "∀ x. s ≡[x] t"
assumes static_eq: "∀ f. s@@(staticLoc f) = t@@(staticLoc f)"
shows "s = t"
proof (rule Store_eqI)
from xeq
show "∀x. alive x s = alive x t"
by (simp add: xeq_def)
next
show "∀l. s@@l = t@@l"
proof
fix l
show "s@@l = t@@l"
proof (cases l)
case (objLoc cf a)
have "l = objLoc cf a" by fact
hence "s⊢ l reachable_from (objV (cls cf) a)"
by simp
with xeq show ?thesis
by (simp add: xeq_def)
next
case (staticLoc f)
have "l = staticLoc f" by fact
with static_eq show ?thesis
by (simp add: xeq_def)
next
case (arrLenLoc T a)
have "l = arrLenLoc T a" by fact
hence "s⊢ l reachable_from (arrV T a)"
by simp
with xeq show ?thesis
by (simp add: xeq_def)
next
case (arrLoc T a i)
have "l = arrLoc T a i" by fact
hence "s⊢ l reachable_from (arrV T a)"
by simp
with xeq show ?thesis
by (simp add: xeq_def)
qed
qed
qed
text ‹Lemma 3.4 (iii)›
lemma xeq3:
assumes unreach_l: "¬ s⊢ l reachable_from x"
shows "s ≡[x] s⟨l:=y⟩"
proof (rule xeqI)
show "alive x s = alive x (s⟨l := y⟩)"
by simp
next
fix k
assume reach_k: "s⊢ k reachable_from x"
with unreach_l have "l≠k" by auto
then show "s@@k = s⟨l := y⟩@@k"
by simp
qed
text ‹Lemma 3.4 (iv)›
lemma xeq4: assumes not_new: "x ≠ new s t"
shows "s ≡[x] s⟨t⟩"
proof (rule xeqI)
from not_new
show "alive x s = alive x (s⟨t⟩)"
by (simp add: alive_alloc_exhaust)
next
fix l
assume reach_l: "s⊢ l reachable_from x"
show "s@@l = s⟨t⟩@@l"
proof (cases "isNewArr t ⟶ l ≠ arr_len (new s t)")
case True
with reach_l show ?thesis
by simp
next
case False
then obtain T n where t: "t = new_array T n" and
l: "l = arr_len (new s t)"
by (cases t) auto
hence "ref l = new s t"
by simp
from this reach_l
have "x = new s t"
by (rule loc_new_reach)
with not_new show ?thesis ..
qed
qed
text ‹Lemma 3.4 (v)›
lemma xeq5: "s ≡[x] t ⟹ s⊢ l reachable_from x = t⊢ l reachable_from x"
by (rule reach9) (simp add: xeq_def)
subsection ‹T-Equivalence›
text ‹T-equivalence is the extension of X-equivalence from values to types. Two stores are
T-equivalent iff they are X-equivalent for all values of type T. This is formalized by the
predicate ‹teq› \<^cite>‹‹p. 55› in "Poetzsch-Heffter97specification"›.›
definition teq:: "Javatype ⇒ Store ⇒ Store ⇒ bool" where
"teq t s1 s2 = (∀ x. typeof x ≤ t ⟶ s1 ≡[x] s2)"
subsection ‹Less Alive›
text ‹To specify that methods have no side-effects, the following binary relation on stores
plays a prominent role. It expresses that the two stores differ only in values that are alive
in the store passed as first argument. This is formalized by the predicate ‹lessalive›
\<^cite>‹‹p. 55› in "Poetzsch-Heffter97specification"›.
The stores have to be X-equivalent for the references of the
first store that are alive, and the values of the static fields have to be the same in both stores.
›
definition lessalive:: "Store ⇒ Store ⇒ bool" ("_/ ≪ _" [70,71] 70)
where "lessalive s t = ((∀ x. alive x s ⟶ s ≡[x] t) ∧ (∀ f. s@@staticLoc f = t@@staticLoc f))"
text ‹We define an introduction rule for the new operator.›
lemma lessaliveI:
"⟦⋀ x. alive x s ⟹ s ≡[x] t; ⋀ f. s@@staticLoc f = t@@staticLoc f⟧
⟹ s ≪ t"
by (simp add: lessalive_def)
text ‹It can be shown that ‹lessalive› is reflexive, transitive and antisymmetric.›
lemma lessalive_refl: "s ≪ s"
by (simp add: lessalive_def xeq1_refl)
lemma lessalive_trans [trans]:
assumes s_t: "s ≪ t"
assumes t_w: "t ≪ w"
shows "s ≪ w"
proof (rule lessaliveI)
fix x
assume alive_x_s: "alive x s"
with s_t have "s ≡[x] t"
by (simp add: lessalive_def)
also
have "t ≡[x] w"
proof -
from alive_x_s s_t have "alive x t" by (simp add: lessalive_def xeq_def)
with t_w show ?thesis
by (simp add: lessalive_def)
qed
finally show "s ≡[x] w".
next
fix f
from s_t t_w show "s@@staticLoc f = w@@staticLoc f"
by (simp add: lessalive_def)
qed
lemma lessalive_antisym:
assumes s_t: "s ≪ t"
assumes t_s: "t ≪ s"
shows "s = t"
proof (rule xeq2)
show "∀x. s ≡[x] t"
proof
fix x show "s ≡[x] t"
proof (cases "alive x s")
case True
with s_t show ?thesis by (simp add: lessalive_def)
next
case False note unalive_x_s = this
show ?thesis
proof (cases "alive x t")
case True
with t_s show ?thesis
by (subst xeq1_sym) (simp add: lessalive_def)
next
case False
show ?thesis
proof (rule xeqI)
from False unalive_x_s show "alive x s = alive x t" by simp
next
fix l assume reach_s_x: "s⊢ l reachable_from x"
with unalive_x_s have x: "x = ref l"
by (rule ref_reach_unalive)
with unalive_x_s have "s@@l = init (ltype l)"
by simp
also from reach_s_x x have "t⊢ l reachable_from x"
by (auto intro: reach.Immediate unreachable_Null)
with False x have "t@@l = init (ltype l)"
by simp
finally show "s@@l = t@@l"
by simp
qed
qed
qed
qed
next
from s_t show "∀f. s@@staticLoc f = t@@staticLoc f"
by (simp add: lessalive_def)
qed
text ‹This gives us a partial ordering on the store. Thus, the type @{typ "Store"}
can be added to the appropriate type class @{term "ord"} which lets us define the $<$ and
$\leq$ symbols, and to the type class @{term "order"} which axiomatizes partial orderings.
›
instantiation Store :: order
begin
definition
le_Store_def: "s ≤ t ⟷ s ≪ t"
definition
less_Store_def: "(s::Store) < t ⟷ s ≤ t ∧ ¬ t ≤ s"
text ‹We prove Lemma 3.5 of \<^cite>‹‹p. 56› in "Poetzsch-Heffter97specification"› for this relation.
›
text ‹Lemma 3.5 (i)›
instance proof
fix s t w:: "Store"
{
show "s ≤ s"
by (simp add: le_Store_def lessalive_refl)
next
assume "s ≤ t" "t ≤ w"
then show "s ≤ w"
by (unfold le_Store_def) (rule lessalive_trans)
next
assume "s ≤ t" "t ≤ s"
then show "s = t"
by (unfold le_Store_def) (rule lessalive_antisym)
next
show "(s < t) = (s ≤ t ∧ ¬ t ≤ s)"
by (simp add: less_Store_def)
}
qed
end
text ‹Lemma 3.5 (ii)›
lemma lessalive2: "⟦s ≪ t; alive x s⟧ ⟹ alive x t"
by (simp add: lessalive_def xeq_def)
text ‹Lemma 3.5 (iii)›
lemma lessalive3:
assumes s_t: "s ≪ t"
assumes alive: "alive x s ∨ ¬ alive x t"
shows "s ≡[x] t"
proof (cases "alive x s")
case True
with s_t show ?thesis
by (simp add: lessalive_def)
next
case False
note unalive_x_s = this
with alive have unalive_x_t: "¬ alive x t"
by simp
show ?thesis
proof (rule xeqI)
from False alive show "alive x s = alive x t"
by simp
next
fix l assume reach_s_x: "s⊢ l reachable_from x"
with unalive_x_s have x: "x = ref l"
by (rule ref_reach_unalive)
with unalive_x_s have "s@@l = init (ltype l)"
by simp
also from reach_s_x x have "t⊢ l reachable_from x"
by (auto intro: reach.Immediate unreachable_Null)
with unalive_x_t x have "t@@l = init (ltype l)"
by simp
finally show "s@@l = t@@l"
by simp
qed
qed
text ‹Lemma 3.5 (iv)›
lemma lessalive_update [simp,intro]:
assumes s_t: "s ≪ t"
assumes unalive_l: "¬ alive (ref l) t"
shows "s ≪ t⟨l:=x⟩"
proof -
from unalive_l have "t⟨l:=x⟩ = t"
by simp
with s_t show ?thesis by simp
qed
lemma Xequ4':
assumes alive: "alive x s"
shows "s ≡[x] s⟨t⟩"
proof -
from alive have "x ≠ new s t"
by auto
thus ?thesis
by (rule xeq4)
qed
text ‹Lemma 3.5 (v)›
lemma lessalive_alloc [simp,intro]: "s ≪ s⟨t⟩"
by (simp add: lessalive_def Xequ4')
subsection ‹Reachability of Types from Types›
text ‹The predicate ‹treach› denotes the fact that the first type reaches
the second type by stepping finitely many times from a type to the range type of one
of its fields. This formalization diverges from \<^cite>‹‹p. 106› in "Poetzsch-Heffter97specification"›
in that it does not include the number of steps that are allowed to reach the second type.
Reachability of types is a static approximation of reachability in
the store. If I cannot reach the type of a location from the type of a
reference, I cannot reach the location from the reference. See lemma
‹not_treach_ref_impl_not_reach› below.
›
inductive
treach :: "Javatype ⇒ Javatype ⇒ bool"
where
Subtype: "U ≤ T ⟹ treach T U"
| Attribute: "⟦treach T S; S ≤ dtype f; U ≤ rtype f⟧ ⟹ treach T U"
| ArrLength: "treach (ArrT AT) IntgT"
| ArrElem: "treach (ArrT AT) (at2jt AT)"
| Trans [trans]: "⟦treach T U; treach U V⟧ ⟹ treach T V"
lemma treach_ref_l [simp,intro]:
assumes not_Null: "ref l ≠ nullV"
shows "treach (typeof (ref l)) (ltype l)"
proof (cases l)
case (objLoc cf a)
have "l=objLoc cf a" by fact
moreover
have "treach (CClassT (cls cf)) (rtype (att cf))"
by (rule treach.Attribute [where ?f="att cf" and ?S="CClassT (cls cf)"])
(auto intro: treach.Subtype)
ultimately show ?thesis
by simp
next
case (staticLoc f)
have "l=staticLoc f" by fact
hence "ref l = nullV" by simp
with not_Null show ?thesis
by simp
next
case (arrLenLoc T a)
have "l=arrLenLoc T a" by fact
then show ?thesis
by (auto intro: treach.ArrLength)
next
case (arrLoc T a i)
have "l=arrLoc T a i" by fact
then show ?thesis
by (auto intro: treach.ArrElem)
qed
lemma treach_ref_l' [simp,intro]:
assumes not_Null: "ref l ≠ nullV"
shows "treach (typeof (ref l)) (typeof (s@@l))"
proof -
from not_Null have "treach (typeof (ref l)) (ltype l)" by (rule treach_ref_l)
also have "typeof (s@@l) ≤ ltype l"
by simp
hence "treach (ltype l) (typeof (s@@l))"
by (rule treach.intros)
finally show ?thesis .
qed
lemma reach_impl_treach:
assumes reach_l: "s ⊢ l reachable_from x"
shows "treach (typeof x) (ltype l)"
using reach_l
proof (induct)
case (Immediate l)
have "ref l ≠ nullV" by fact
then show "treach (typeof (ref l)) (ltype l)"
by (rule treach_ref_l)
next
case (Indirect l k)
have "treach (typeof (s@@k)) (ltype l)" by fact
moreover
have "ref k ≠ nullV" by fact
hence "treach (typeof (ref k)) (typeof (s@@k))"
by simp
ultimately show "treach (typeof (ref k)) (ltype l)"
by (iprover intro: treach.Trans)
qed
lemma not_treach_ref_impl_not_reach:
assumes not_treach: "¬ treach (typeof x) (typeof (ref l))"
shows "¬ s ⊢ l reachable_from x"
proof
assume reach_l: "s⊢ l reachable_from x"
from this not_treach
show False
proof (induct)
case (Immediate l)
have "¬ treach (typeof (ref l)) (typeof (ref l))" by fact
thus False by (iprover intro: treach.intros order_refl)
next
case (Indirect l k)
have hyp: "¬ treach (typeof (s@@k)) (typeof (ref l)) ⟹ False" by fact
have not_Null: "ref k ≠ nullV" by fact
have not_k_l:"¬ treach (typeof (ref k)) (typeof (ref l))" by fact
show False
proof (cases "treach (typeof (s@@k)) (typeof (ref l))")
case False thus False by (rule hyp)
next
case True
from not_Null have "treach (typeof (ref k)) (typeof (s@@k))"
by (rule treach_ref_l')
also note True
finally have "treach (typeof (ref k)) (typeof (ref l))" .
with not_k_l show False ..
qed
qed
qed
text ‹Lemma 4.6 in \<^cite>‹‹p. 107› in "Poetzsch-Heffter97specification"›.›
lemma treach1:
assumes x_t: "typeof x ≤ T"
assumes not_treach: "¬ treach T (typeof (ref l))"
shows "¬ s ⊢ l reachable_from x"
proof -
have "¬ treach (typeof x) (typeof (ref l))"
proof
from x_t have "treach T (typeof x)" by (rule treach.intros)
also assume "treach (typeof x) (typeof (ref l))"
finally have "treach T (typeof (ref l))" .
with not_treach show False ..
qed
thus ?thesis
by (rule not_treach_ref_impl_not_reach)
qed
end