# Theory DynamicControlDependences

```section ‹Interpretations of the various dynamic control dependences›

theory DynamicControlDependences imports AdditionalLemmas "../Dynamic/DynPDG" begin

interpretation WDynStandardControlDependence:
DynStandardControlDependencePDG sourcenode targetnode kind "valid_edge prog"
Entry "Defs prog" "Uses prog" id Exit
for prog
proof(unfold_locales)
fix n assume "CFG.valid_node sourcenode targetnode (valid_edge prog) n"
hence "valid_node prog n" by(simp add:valid_node_def While_CFG.valid_node_def)
thus "∃as. prog ⊢ (_Entry_) -as→* n" by(rule valid_node_Entry_path)
next
fix n assume "CFG.valid_node sourcenode targetnode (valid_edge prog) n"
hence "valid_node prog n" by(simp add:valid_node_def While_CFG.valid_node_def)
thus "∃as. prog ⊢ n -as→* (_Exit_)" by(rule valid_node_Exit_path)
qed

interpretation WDynWeakControlDependence:
DynWeakControlDependencePDG sourcenode targetnode kind "valid_edge prog"
Entry "Defs prog" "Uses prog" id Exit
for prog
proof(unfold_locales)
fix n assume "CFG.valid_node sourcenode targetnode (valid_edge prog) n"
hence "valid_node prog n" by(simp add:valid_node_def While_CFG.valid_node_def)
show "finite {n'. ∃a'. valid_edge prog a' ∧ sourcenode a' = n ∧
targetnode a' = n'}"
by(rule finite_successors)
qed

end
```