| author | paulson |
| Fri, 15 Sep 2000 12:39:57 +0200 | |
| changeset 9969 | 4753185f1dd2 |
| parent 8034 | 6fc37b5c5e98 |
| child 10042 | 7164dc0d24d8 |
| permissions | -rw-r--r-- |
| 8011 | 1 |
(* Title: HOL/MicroJava/JVM/JVMState.thy |
2 |
ID: $Id$ |
|
3 |
Author: Cornelia Pusch |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
State of the JVM |
|
7 |
*) |
|
8 |
||
9 |
JVMState = Store + |
|
10 |
||
11 |
||
12 |
(** frame stack **) |
|
13 |
||
14 |
types |
|
15 |
opstack = "val list" |
|
16 |
locvars = "val list" |
|
17 |
p_count = nat |
|
18 |
||
19 |
frame = "opstack \\<times> |
|
20 |
locvars \\<times> |
|
21 |
cname \\<times> |
|
22 |
sig \\<times> |
|
23 |
p_count" |
|
24 |
||
25 |
(* operand stack *) |
|
26 |
(* local variables *) |
|
27 |
(* name of def. class defined *) |
|
28 |
(* meth name+param_desc *) |
|
29 |
(* program counter within frame *) |
|
30 |
||
31 |
||
32 |
(** exceptions **) |
|
33 |
||
34 |
constdefs |
|
35 |
raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option" |
|
36 |
"raise_xcpt c x \\<equiv> (if c then Some x else None)" |
|
37 |
||
38 |
(** runtime state **) |
|
39 |
||
40 |
types |
|
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8011
diff
changeset
|
41 |
jvm_state = "xcpt option \\<times> aheap \\<times> frame list" |
| 8011 | 42 |
|
43 |
||
44 |
||
45 |
(** dynamic method lookup **) |
|
46 |
||
47 |
constdefs |
|
48 |
dyn_class :: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname" |
|
|
8034
6fc37b5c5e98
Various little changes like cmethd -> method and cfield -> field.
nipkow
parents:
8011
diff
changeset
|
49 |
"dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(method(G,C) sig))" |
| 8011 | 50 |
end |