author | wenzelm |
Tue, 16 Jan 2018 09:30:00 +0100 | |
changeset 67443 | 3abf6a722518 |
parent 62042 | 6c6ccf573479 |
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 |
||
61361 | 5 |
chapter \<open>Java Virtual Machine \label{cha:jvm}\<close> |
58886 | 6 |
|
61361 | 7 |
section \<open>State of the JVM\<close> |
8011 | 8 |
|
15860 | 9 |
theory JVMState |
10 |
imports "../J/Conform" |
|
11 |
begin |
|
8011 | 12 |
|
61361 | 13 |
subsection \<open>Frame Stack\<close> |
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 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
25 |
\<comment> \<open>operand stack\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
26 |
\<comment> \<open>local variables (including this pointer and method parameters)\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
27 |
\<comment> \<open>name of class where current method is defined\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
28 |
\<comment> \<open>method name + parameter types\<close> |
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
29 |
\<comment> \<open>program counter within frame\<close> |
12519 | 30 |
|
31 |
||
61361 | 32 |
subsection \<open>Exceptions\<close> |
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 |
|
61361 | 36 |
subsection \<open>Runtime State\<close> |
42463 | 37 |
type_synonym |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
38 |
jvm_state = "val option \<times> aheap \<times> frame list" \<comment> \<open>exception flag, heap, frames\<close> |
8011 | 39 |
|
40 |
||
61361 | 41 |
subsection \<open>Lemmas\<close> |
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 |