author | kleing |
Sun, 16 Dec 2001 00:19:08 +0100 | |
changeset 12519 | a955fe2879ba |
parent 11177 | 749fd046002f |
child 12911 | 704713ca07ea |
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 |
||
10057 | 7 |
header {* State of the JVM *} |
8011 | 8 |
|
10922
f1209aff9517
Store.thy is obsolete (newref isn't used any more)
kleing
parents:
10057
diff
changeset
|
9 |
theory JVMState = Conform: |
8011 | 10 |
|
12519 | 11 |
section {* Frame Stack *} |
8011 | 12 |
types |
12519 | 13 |
opstack = "val list" |
14 |
locvars = "val list" |
|
15 |
p_count = nat |
|
8011 | 16 |
|
12519 | 17 |
frame = "opstack \<times> |
18 |
locvars \<times> |
|
19 |
cname \<times> |
|
20 |
sig \<times> |
|
10057 | 21 |
p_count" |
8011 | 22 |
|
12519 | 23 |
-- "operand stack" |
24 |
-- "local variables (including this pointer and method parameters)" |
|
25 |
-- "name of class where current method is defined" |
|
26 |
-- "method name + parameter types" |
|
27 |
-- "program counter within frame" |
|
28 |
||
29 |
||
30 |
section {* Exceptions *} |
|
31 |
constdefs |
|
32 |
raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" |
|
33 |
"raise_system_xcpt b x == if b then Some (Addr (XcptRef x)) else None" |
|
34 |
||
35 |
-- "redefines State.new\\_Addr:" |
|
36 |
new_Addr :: "aheap => loc \<times> val option" |
|
37 |
"new_Addr h == SOME (a,x). (h a = None \<and> x = None) | |
|
38 |
x = raise_system_xcpt True OutOfMemory" |
|
39 |
||
40 |
||
41 |
section {* Runtime State *} |
|
42 |
types |
|
43 |
jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |
|
8011 | 44 |
|
45 |
||
12519 | 46 |
section {* Lemmas *} |
8011 | 47 |
|
12519 | 48 |
lemma new_AddrD: |
49 |
"new_Addr hp = (ref, xcp) \<Longrightarrow> hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))" |
|
50 |
apply (drule sym) |
|
51 |
apply (unfold new_Addr_def) |
|
52 |
apply (simp add: raise_system_xcpt_def) |
|
53 |
apply (simp add: Pair_fst_snd_eq Eps_split) |
|
54 |
apply (rule someI) |
|
55 |
apply (rule disjI2) |
|
56 |
apply (rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans) |
|
57 |
apply auto |
|
58 |
done |
|
8011 | 59 |
|
12519 | 60 |
lemma new_Addr_OutOfMemory: |
61 |
"snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
|
62 |
proof - |
|
63 |
obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp") |
|
64 |
moreover |
|
65 |
assume "snd (new_Addr hp) = Some xcp" |
|
66 |
ultimately |
|
67 |
show ?thesis by (auto dest: new_AddrD) |
|
68 |
qed |
|
69 |
||
70 |
end |