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