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