Theory JVMState

(*  Title:      Jinja/JVM/JVMState.thy
    ID:         $Id: JVMState.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Cornelia Pusch, Gerwin Klein
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* 
  \chapter{Jinja Virtual Machine}\label{cha:jvm}
  \isaheader{State of the JVM} 
*}

theory JVMState = Objects:

section {* Frame Stack *}

types 
  pc = nat

  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 *}
types
  jvm_state = "addr option × heap × frame list"  
  -- "exception flag, heap, frames"
  
end