Theory JVMSDG

theory JVMSDG imports JVMCFG_wf JVMPostdomination "../StaticInter/SDG" begin

interpretation JVMCFGExit_wf_new_type:
  CFGExit_wf "sourcenode" "targetnode" "kind" "valid_edge⇘CFG⇙ P"
  "(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, Enter)"
  "(λ(C, M, pc, type). (C, M))" "get_return_edges (fst⇘CFG⇙ P)"
  "((ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P)),[],[]) # procs (PROG (fst⇘CFG⇙ P))"
  "(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P))"
  "(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, Return)"
  "Def (fst⇘CFG⇙ P)" "Use (fst⇘CFG⇙ P)" "ParamDefs (fst⇘CFG⇙ P)" "ParamUses (fst⇘CFG⇙ P)"
  for P
  unfolding valid_edge_CFG_def
  ..

interpretation JVM_SDG :
  SDG "sourcenode" "targetnode" "kind" "valid_edge⇘CFG⇙ P"
  "(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, Enter)"
  "(λ(C, M, pc, type). (C, M))" "get_return_edges (fst⇘CFG⇙ P)"
  "((ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P)),[],[]) # procs (PROG (fst⇘CFG⇙ P))"
  "(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P))"
  "(ClassMain (fst⇘CFG⇙ P), MethodMain (fst⇘CFG⇙ P), None, Return)"
  "Def (fst⇘CFG⇙ P)" "Use (fst⇘CFG⇙ P)" "ParamDefs (fst⇘CFG⇙ P)" "ParamUses (fst⇘CFG⇙ P)"
  for P
  ..

end