Theory JVMState

(*  Title:      JinjaThreads/JVM/JVMState.thy
    Author:     Cornelia Pusch, Gerwin Klein, Andreas Lochbihler
*)

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

theory JVMState imports
  "../Common/Objects"
  "../Framework/FWState"
  "../Common/Observable_Events"
begin

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"

translations
  "frame" <= (type) "val list × val list × String.literal × String.literal × nat"

section {* Runtime State *}
types
  jvm_state = "addr option × heap × frame list"  
  -- "exception flag, heap, frames"

types
  jvm_thread_state = "addr option × frame list"
  -- "exception flag, frames, thread lock state"

types
  jvm_thread_action = "(addr,thread_id,jvm_thread_state,heap,addr,obs_event option) thread_action"
  jvm_ta_state = "jvm_thread_action × jvm_state"

translations
  "jvm_thread_action" <= (type) "(nat,nat,nat option × frame list,heap,nat,obs_event option) thread_action"

end