Up to index of Isabelle/HOL/Jinja/HRB-Slicing
theory JVMSDGtheory 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