Theory Slicing.WeakControlDependence

section ‹Static Weak Control Dependence›

theory WeakControlDependence imports 
  "../Basic/Postdomination" 
  "../Basic/DynWeakControlDependence"
begin

context StrongPostdomination begin

definition 
  weak_control_dependence :: "'node  'node  bool" 
  ("_ weakly controls _" [51,0])
where weak_control_dependences_eq:
    "n weakly controls n'  as. n weakly controls n' via as"

lemma 
  weak_control_dependence_def:"n weakly controls n' = 
    (a a' as. (n'  set(sourcenodes (a#as)))  (n -a#as→* n') 
                   (n' strongly-postdominates (targetnode a)) 
                   (valid_edge a')  (sourcenode a' = n)  
                   (¬ n' strongly-postdominates (targetnode a')))"
by(auto simp:weak_control_dependences_eq dyn_weak_control_dependence_def)


lemma Exit_not_weak_control_dependent:
  "n weakly controls (_Exit_)  False"
by(auto simp:weak_control_dependences_eq 
        intro:Exit_not_dyn_weak_control_dependent)

end

end