Up to index of Isabelle/HOL/Jinja/Slicing
theory WeakOrderDependenceheader {* \isaheader{Weak Order Dependence} *}
theory WeakOrderDependence imports "../Basic/CFG" DataDependence begin
text {* Weak order dependence is just defined as a static control dependence *}
subsection{* Definition and some lemmas *}
definition (in CFG) weak_order_dependence :: "'node => 'node => 'node => bool"
("_ -->⇘wod⇙ _,_")
where wod_def:"n -->⇘wod⇙ n⇣1,n⇣2 ≡ ((n⇣1 ≠ n⇣2) ∧
(∃as. (n -as->* n⇣1) ∧ (n⇣2 ∉ set (sourcenodes as))) ∧
(∃as. (n -as->* n⇣2) ∧ (n⇣1 ∉ set (sourcenodes as))) ∧
(∃a. (valid_edge a) ∧ (n = sourcenode a) ∧
((∃as. (targetnode a -as->* n⇣1) ∧
(∀as'. (targetnode a -as'->* n⇣2) --> n⇣1 ∈ set(sourcenodes as'))) ∨
(∃as. (targetnode a -as->* n⇣2) ∧
(∀as'. (targetnode a -as'->* n⇣1) --> n⇣2 ∈ set(sourcenodes as'))))))"
inductive_set (in CFG_wf) wod_backward_slice :: "'node set => 'node set"
for S :: "'node set"
where refl:"[|valid_node n; n ∈ S|] ==> n ∈ wod_backward_slice S"
| cd_closed:
"[|n' -->⇘wod⇙ n⇣1,n⇣2; n⇣1 ∈ wod_backward_slice S; n⇣2 ∈ wod_backward_slice S|]
==> n' ∈ wod_backward_slice S"
| dd_closed:"[|n' influences V in n''; n'' ∈ wod_backward_slice S|]
==> n' ∈ wod_backward_slice S"
lemma (in CFG_wf)
wod_backward_slice_valid_node:"n ∈ wod_backward_slice S ==> valid_node n"
by(induct rule:wod_backward_slice.induct,
auto dest:path_valid_node simp:wod_def data_dependence_def)
end