src/HOL/MicroJava/JVM/JVMState.thy
author wenzelm
Thu Oct 04 20:29:42 2007 +0200 (2007-10-04)
changeset 24850 0cfd722ab579
parent 15860 a344c4284972
child 35416 d8d7d1b785af
permissions -rw-r--r--
Name.uu, Name.aT;
     1 (*  Title:      HOL/MicroJava/JVM/JVMState.thy
     2     ID:         $Id$
     3     Author:     Cornelia Pusch, Gerwin Klein
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header {* 
     8   \chapter{Java Virtual Machine}\label{cha:jvm}
     9   \isaheader{State of the JVM} 
    10 *}
    11 
    12 theory JVMState
    13 imports "../J/Conform"
    14 begin
    15 
    16 section {* Frame Stack *}
    17 types
    18  opstack   = "val list"
    19  locvars   = "val list" 
    20  p_count   = nat
    21 
    22  frame = "opstack \<times>     
    23           locvars \<times>   
    24           cname \<times>     
    25           sig \<times>     
    26           p_count"
    27 
    28   -- "operand stack" 
    29   -- "local variables (including this pointer and method parameters)"
    30   -- "name of class where current method is defined"
    31   -- "method name + parameter types"
    32   -- "program counter within frame"
    33 
    34 
    35 section {* Exceptions *}
    36 constdefs
    37   raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option"
    38   "raise_system_xcpt b x \<equiv> raise_if b x None"
    39 
    40 section {* Runtime State *}
    41 types
    42   jvm_state = "val option \<times> aheap \<times> frame list"  -- "exception flag, heap, frames"
    43 
    44 
    45 section {* Lemmas *}
    46 
    47 lemma new_Addr_OutOfMemory:
    48   "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)"
    49 proof - 
    50   obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp")
    51   moreover
    52   assume "snd (new_Addr hp) = Some xcp" 
    53   ultimately
    54   show ?thesis by (auto dest: new_AddrD)
    55 qed
    56   
    57 end