header {*
\chapter{Jinja Virtual Machine}\label{cha:jvm}
\isaheader{State of the JVM}
*}
theory JVMState imports "../Common/Objects" begin
section {* Frame Stack *}
type_synonym
pc = nat
type_synonym
frame = "val list × val list × cname × mname × pc"
-- "operand stack"
-- "registers (including this pointer, method parameters, and local variables)"
-- "name of class where current method is defined"
-- "parameter types"
-- "program counter within frame"
section {* Runtime State *}
type_synonym
jvm_state = "addr option × heap × frame list"
-- "exception flag, heap, frames"
end