Theory Slicing.DataDependence

section ‹Static data dependence›

theory DataDependence imports "../Basic/DynDataDependence" begin

context CFG_wf begin

definition data_dependence :: "'node  'var  'node  bool"
    (‹_ influences _ in _› [51,0])
where data_dependences_eq:"n influences V in n'  as. n influences V in n' via as"

lemma data_dependence_def: "n influences V in n' = 
  (a' as'. (V  Def n)  (V  Use n') 
                 (n -a'#as'→* n')  (n''  set (sourcenodes as'). V  Def n''))"
by(auto simp:data_dependences_eq dyn_data_dependence_def)

end

end