author | wenzelm |
Sun, 02 Nov 2014 17:58:35 +0100 | |
changeset 58886 | 8a6cac7c7247 |
parent 42463 | f270e3e18be5 |
child 61361 | 8b5f00202e1a |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/JVM/JVMState.thy |
41589 | 2 |
Author: Cornelia Pusch, Gerwin Klein, Technische Universitaet Muenchen |
8011 | 3 |
*) |
4 |
||
58886 | 5 |
chapter {* Java Virtual Machine \label{cha:jvm} *} |
6 |
||
7 |
section {* State of the JVM *} |
|
8011 | 8 |
|
15860 | 9 |
theory JVMState |
10 |
imports "../J/Conform" |
|
11 |
begin |
|
8011 | 12 |
|
58886 | 13 |
subsection {* Frame Stack *} |
42463 | 14 |
type_synonym opstack = "val list" |
15 |
type_synonym locvars = "val list" |
|
16 |
type_synonym p_count = nat |
|
8011 | 17 |
|
42463 | 18 |
type_synonym |
12519 | 19 |
frame = "opstack \<times> |
20 |
locvars \<times> |
|
21 |
cname \<times> |
|
22 |
sig \<times> |
|
10057 | 23 |
p_count" |
8011 | 24 |
|
12519 | 25 |
-- "operand stack" |
26 |
-- "local variables (including this pointer and method parameters)" |
|
27 |
-- "name of class where current method is defined" |
|
28 |
-- "method name + parameter types" |
|
29 |
-- "program counter within frame" |
|
30 |
||
31 |
||
58886 | 32 |
subsection {* Exceptions *} |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
15860
diff
changeset
|
33 |
definition raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" where |
13674 | 34 |
"raise_system_xcpt b x \<equiv> raise_if b x None" |
12519 | 35 |
|
58886 | 36 |
subsection {* Runtime State *} |
42463 | 37 |
type_synonym |
12519 | 38 |
jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |
8011 | 39 |
|
40 |
||
58886 | 41 |
subsection {* Lemmas *} |
8011 | 42 |
|
12519 | 43 |
lemma new_Addr_OutOfMemory: |
44 |
"snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
|
45 |
proof - |
|
46 |
obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp") |
|
47 |
moreover |
|
48 |
assume "snd (new_Addr hp) = Some xcp" |
|
49 |
ultimately |
|
50 |
show ?thesis by (auto dest: new_AddrD) |
|
13052 | 51 |
qed |
52 |
||
13674 | 53 |
end |