Theory JVMState

(*  Title:      Jinja/JVM/JVMState.thy

    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

chapter ‹Jinja Virtual Machine \label{cha:jvm}›

section ‹State of the JVM›

theory JVMState imports "../Common/Objects" begin

subsection ‹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›

subsection ‹Runtime State›

type_synonym
  jvm_state = "addr option × heap × frame list"  
  ― ‹exception flag, heap, frames›
  
end