Theory 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