Quelle  JVMState.thy   Sprache: Isabelle

(*  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