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"
   ("_ wod _,_")
where wod_def:"n wod n1,n2  ((n1  n2) 
   (as. (n -as→* n1)  (n2  set (sourcenodes as))) 
   (as. (n -as→* n2)  (n1  set (sourcenodes as))) 
   (a. (valid_edge a)  (n = sourcenode a)  
        ((as. (targetnode a -as→* n1)   
               (as'. (targetnode a -as'→* n2)  n1  set(sourcenodes as'))) 
         (as. (targetnode a -as→* n2)   
               (as'. (targetnode a -as'→* n1)  n2  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 n1,n2; n1  wod_backward_slice S; n2  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