author | kleing |
Thu, 21 Mar 2002 12:58:31 +0100 | |
changeset 13063 | b1789117a1c6 |
parent 13052 | 3bf41c474a88 |
child 13674 | f4c64597fb02 |
permissions | -rw-r--r-- |
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 |
|
10922
f1209aff9517
Store.thy is obsolete (newref isn't used any more)
kleing
parents:
10057
diff
changeset
|
12 |
theory JVMState = Conform: |
8011 | 13 |
|
12519 | 14 |
section {* Frame Stack *} |
8011 | 15 |
types |
12519 | 16 |
opstack = "val list" |
17 |
locvars = "val list" |
|
18 |
p_count = nat |
|
8011 | 19 |
|
12519 | 20 |
frame = "opstack \<times> |
21 |
locvars \<times> |
|
22 |
cname \<times> |
|
23 |
sig \<times> |
|
10057 | 24 |
p_count" |
8011 | 25 |
|
12519 | 26 |
-- "operand stack" |
27 |
-- "local variables (including this pointer and method parameters)" |
|
28 |
-- "name of class where current method is defined" |
|
29 |
-- "method name + parameter types" |
|
30 |
-- "program counter within frame" |
|
31 |
||
32 |
||
33 |
section {* Exceptions *} |
|
34 |
constdefs |
|
35 |
raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" |
|
13063
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
36 |
"raise_system_xcpt b x \<equiv> if b then Some (Addr (XcptRef x)) else None" |
12519 | 37 |
|
38 |
-- "redefines State.new\\_Addr:" |
|
13063
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
39 |
new_Addr :: "aheap \<Rightarrow> loc \<times> val option" |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
40 |
"new_Addr h \<equiv> let (a, x) = State.new_Addr h |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
41 |
in (a, raise_system_xcpt (x ~= None) OutOfMemory)" |
12519 | 42 |
|
43 |
||
44 |
section {* Runtime State *} |
|
45 |
types |
|
46 |
jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |
|
8011 | 47 |
|
48 |
||
13052 | 49 |
text {* a new, blank object with default values in all fields: *} |
50 |
constdefs |
|
51 |
blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" |
|
52 |
"blank G C \<equiv> (C,init_vars (fields(G,C)))" |
|
53 |
||
54 |
start_heap :: "'c prog \<Rightarrow> aheap" |
|
55 |
"start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) |
|
13063
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
56 |
(XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
57 |
(XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" |
13052 | 58 |
|
12519 | 59 |
section {* Lemmas *} |
8011 | 60 |
|
12519 | 61 |
lemma new_AddrD: |
13063
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
62 |
assumes new: "new_Addr hp = (ref, xcp)" |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
63 |
shows "hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))" |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
64 |
proof - |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
65 |
from new obtain xcpT where old: "State.new_Addr hp = (ref,xcpT)" |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
66 |
by (cases "State.new_Addr hp") (simp add: new_Addr_def) |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
67 |
from this [symmetric] |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
68 |
have "hp ref = None \<and> xcpT = None \<or> xcpT = Some OutOfMemory" |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
69 |
by (rule State.new_AddrD) |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
70 |
with new old show ?thesis |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
71 |
by (auto simp add: new_Addr_def raise_system_xcpt_def) |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
72 |
qed |
b1789117a1c6
new_Addr defined in terms of J/State.new_Addr (for compiler)
kleing
parents:
13052
diff
changeset
|
73 |
|
8011 | 74 |
|
12519 | 75 |
lemma new_Addr_OutOfMemory: |
76 |
"snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
|
77 |
proof - |
|
78 |
obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp") |
|
79 |
moreover |
|
80 |
assume "snd (new_Addr hp) = Some xcp" |
|
81 |
ultimately |
|
82 |
show ?thesis by (auto dest: new_AddrD) |
|
13052 | 83 |
qed |
84 |
||
12519 | 85 |
end |