(*  Title:      HOL/MicroJava/JVM/JVMState.thy
    Author:     Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen
*)

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

section ‹State of the JVM›

theory JVMState
imports "../J/Conform"
begin

subsection ‹Frame Stack›
type_synonym opstack = "val list"
type_synonym locvars = "val list"
type_synonym p_count = nat

type_synonym
 frame = "opstack ×
          locvars ×
          cname ×
          sig ×
          p_count"

  ― ‹operand stack›
  ― ‹local variables (including this pointer and method parameters)›
  ― ‹name of class where current method is defined›
  ― ‹method name + parameter types›
  ― ‹program counter within frame›


subsection ‹Exceptions›
definition raise_system_xcpt :: "bool → xcpt → val option" where
  "raise_system_xcpt b x ≡ raise_if b x None"

subsection ‹Runtime State›
type_synonym
  jvm_state = "val option × aheap × frame list"  ― ‹exception flag, heap, frames›


subsection ‹Lemmas›

lemma new_Addr_OutOfMemory:
  "snd (new_Addr hp) = Some xcp ==> xcp = Addr (XcptRef OutOfMemory)"
proof - 
  obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp")
  moreover
  assume "snd (new_Addr hp) = Some xcp" 
  ultimately
  show ?thesis by (auto dest: new_AddrD)
qed
  
end