Theory Slicing.DynWeakControlDependence
section ‹Dynamic Weak Control Dependence›
theory DynWeakControlDependence imports Postdomination begin
context StrongPostdomination begin
definition
dyn_weak_control_dependence :: "'node ⇒ 'node ⇒ 'edge list ⇒ bool"
(‹_ weakly controls _ via _› [51,0,0])
where dyn_weak_control_dependence_def:"n weakly controls n' via as ≡
(∃a a' as'. (as = a#as') ∧ (n' ∉ set(sourcenodes as)) ∧ (n -as→* n') ∧
(n' strongly-postdominates (targetnode a)) ∧
(valid_edge a') ∧ (sourcenode a' = n) ∧
(¬ n' strongly-postdominates (targetnode a')))"
lemma Exit_not_dyn_weak_control_dependent:
assumes control:"n weakly controls (_Exit_) via as" shows "False"
proof -
from control obtain as a as' where path:"n -as→* (_Exit_)" and as:"as = a#as'"
and pd:"(_Exit_) postdominates (targetnode a)"
by(auto simp:dyn_weak_control_dependence_def strong_postdominate_def)
from path as have "n -[]@a#as'→* (_Exit_)" by simp
hence "valid_edge a" by(fastforce dest:path_split)
with pd show False by -(rule Exit_no_postdominator,auto)
qed
end
end