Theory 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