Theory JVMControlDependences

header {* \isaheader{Instantiating the control dependences} *}

theory JVMControlDependences imports
  JVMPostdomination
  JVMCFG_wf
  "../Dynamic/DynPDG"
  "../StaticIntra/CDepInstantiations"
begin

subsection {* Dynamic dependences *}

interpretation JVMDynStandardControlDependence:
  DynStandardControlDependencePDG "sourcenode" "targetnode" "kind" 
  "valid_edge⇘CFG⇙ prog" "(_Entry_)" "Def (fst⇘CFG⇙ prog)" "Use (fst⇘CFG⇙ prog)" 
  "state_val" "(_Exit_)" .. 

interpretation JVMDynWeakControlDependence:
  DynWeakControlDependencePDG "sourcenode" "targetnode" "kind" 
  "valid_edge⇘CFG⇙ prog" "(_Entry_)" "Def (fst⇘CFG⇙ prog)" "Use (fst⇘CFG⇙ prog)" 
  "state_val" "(_Exit_)" ..

subsection {* Static dependences *}

interpretation JVMStandardControlDependence:
  StandardControlDependencePDG "sourcenode" "targetnode" "kind" 
  "valid_edge⇘CFG⇙ prog" "(_Entry_)" "Def (fst⇘CFG⇙ prog)" "Use (fst⇘CFG⇙ prog)" 
  "state_val" "(_Exit_)" ..

interpretation JVMWeakControlDependence:
  WeakControlDependencePDG "sourcenode" "targetnode" "kind" 
  "valid_edge⇘CFG⇙ prog" "(_Entry_)" "Def (fst⇘CFG⇙ prog)" "Use (fst⇘CFG⇙ prog)" 
  "state_val" "(_Exit_)" ..

end