Theory Slicing.WeakOrderDependence
section ‹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"
(‹_ ⟶⇩w⇩o⇩d _,_›)
where wod_def:"n ⟶⇩w⇩o⇩d 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' ⟶⇩w⇩o⇩d 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