# Theory StaticControlDependences

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

theory StaticControlDependences imports
SemanticsWellFormed
begin

lemma WhilePostdomination_aux:
"Postdomination sourcenode targetnode kind (valid_edge prog) Entry Exit"
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 WhilePostdomination:
Postdomination sourcenode targetnode kind "valid_edge prog" Entry Exit
by(rule WhilePostdomination_aux)

lemma WhileStrongPostdomination_aux:
"StrongPostdomination sourcenode targetnode kind (valid_edge prog) Entry Exit"
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

interpretation WhileStrongPostdomination:
StrongPostdomination sourcenode targetnode kind "valid_edge prog" Entry Exit
by(rule WhileStrongPostdomination_aux)

subsection ‹Standard Control Dependence›

lemma WStandardControlDependence_aux:
"StandardControlDependencePDG sourcenode targetnode kind (valid_edge prog)
Entry (Defs prog) (Uses prog) id Exit"
by(unfold_locales)

interpretation WStandardControlDependence:
StandardControlDependencePDG sourcenode targetnode kind "valid_edge prog"
Entry "Defs prog" "Uses prog" id Exit
by(rule WStandardControlDependence_aux)

lemma Fundamental_property_scd_aux: "BackwardSlice_wf sourcenode targetnode kind
(valid_edge prog) Entry (Defs prog) (Uses prog) id
(WStandardControlDependence.PDG_BS_s prog) reds (labels_nodes prog)"
proof -
interpret BackwardSlice sourcenode targetnode kind "valid_edge prog" Entry
"Defs prog" "Uses prog" id
"StandardControlDependencePDG.PDG_BS_s sourcenode targetnode
(valid_edge prog) (Defs prog) (Uses prog) Exit"
by(rule WStandardControlDependence.PDGBackwardSliceCorrect)
show ?thesis by(unfold_locales)
qed

interpretation Fundamental_property_scd: BackwardSlice_wf sourcenode targetnode kind
"valid_edge prog" Entry "Defs prog" "Uses prog" id
"WStandardControlDependence.PDG_BS_s prog" reds "labels_nodes prog"
by(rule Fundamental_property_scd_aux)

subsection ‹Weak Control Dependence›

lemma WWeakControlDependence_aux:
"WeakControlDependencePDG sourcenode targetnode kind (valid_edge prog)
Entry (Defs prog) (Uses prog) id Exit"
by(unfold_locales)

interpretation WWeakControlDependence:
WeakControlDependencePDG sourcenode targetnode kind "valid_edge prog"
Entry "Defs prog" "Uses prog" id Exit
by(rule WWeakControlDependence_aux)

lemma Fundamental_property_wcd_aux: "BackwardSlice_wf sourcenode targetnode kind
(valid_edge prog) Entry (Defs prog) (Uses prog) id
(WWeakControlDependence.PDG_BS_w prog) reds (labels_nodes prog)"
proof -
interpret BackwardSlice sourcenode targetnode kind "valid_edge prog" Entry
"Defs prog" "Uses prog" id
"WeakControlDependencePDG.PDG_BS_w sourcenode targetnode
(valid_edge prog) (Defs prog) (Uses prog) Exit"
by(rule WWeakControlDependence.WeakPDGBackwardSliceCorrect)
show ?thesis by(unfold_locales)
qed

interpretation Fundamental_property_wcd: BackwardSlice_wf sourcenode targetnode kind
"valid_edge prog" Entry "Defs prog" "Uses prog" id
"WWeakControlDependence.PDG_BS_w prog" reds "labels_nodes prog"
by(rule Fundamental_property_wcd_aux)

subsection ‹Weak Order Dependence›

lemma Fundamental_property_wod_aux: "BackwardSlice_wf sourcenode targetnode kind
(valid_edge prog) Entry (Defs prog) (Uses prog) id
(While_CFG_wf.wod_backward_slice prog) reds (labels_nodes prog)"
proof -
interpret BackwardSlice sourcenode targetnode kind "valid_edge prog" Entry
"Defs prog" "Uses prog" id
"CFG_wf.wod_backward_slice sourcenode targetnode (valid_edge prog)
(Defs prog) (Uses prog)"
by(rule While_CFG_wf.WODBackwardSliceCorrect)
show ?thesis by(unfold_locales)
qed

interpretation Fundamental_property_wod: BackwardSlice_wf sourcenode targetnode kind
"valid_edge prog" Entry "Defs prog" "Uses prog" id
"While_CFG_wf.wod_backward_slice prog" reds "labels_nodes prog"
by(rule Fundamental_property_wod_aux)

end
```