8011
|
1 |
(* Title: HOL/MicroJava/JVM/JVMState.thy
|
|
2 |
ID: $Id$
|
12519
|
3 |
Author: Cornelia Pusch, Gerwin Klein
|
8011
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
|
12911
|
7 |
header {*
|
|
8 |
\chapter{Java Virtual Machine}\label{cha:jvm}
|
|
9 |
\isaheader{State of the JVM}
|
|
10 |
*}
|
8011
|
11 |
|
15860
|
12 |
theory JVMState
|
|
13 |
imports "../J/Conform"
|
|
14 |
begin
|
8011
|
15 |
|
12519
|
16 |
section {* Frame Stack *}
|
8011
|
17 |
types
|
12519
|
18 |
opstack = "val list"
|
|
19 |
locvars = "val list"
|
|
20 |
p_count = nat
|
8011
|
21 |
|
12519
|
22 |
frame = "opstack \<times>
|
|
23 |
locvars \<times>
|
|
24 |
cname \<times>
|
|
25 |
sig \<times>
|
10057
|
26 |
p_count"
|
8011
|
27 |
|
12519
|
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"
|
13674
|
38 |
"raise_system_xcpt b x \<equiv> raise_if b x None"
|
12519
|
39 |
|
|
40 |
section {* Runtime State *}
|
|
41 |
types
|
|
42 |
jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames"
|
8011
|
43 |
|
|
44 |
|
12519
|
45 |
section {* Lemmas *}
|
8011
|
46 |
|
12519
|
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)
|
13052
|
55 |
qed
|
|
56 |
|
13674
|
57 |
end
|