1 (* Title: HOL/MicroJava/JVM/JVMState.thy |
1 (* Title: HOL/MicroJava/JVM/JVMState.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Cornelia Pusch |
3 Author: Cornelia Pusch |
4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 |
|
6 State of the JVM |
|
7 *) |
5 *) |
8 |
6 |
9 JVMState = Store + |
7 |
|
8 header {* State of the JVM *} |
10 |
9 |
11 |
10 |
12 (** frame stack **) |
11 theory JVMState = Store: |
13 |
12 |
|
13 |
|
14 text {* frame stack :*} |
14 types |
15 types |
15 opstack = "val list" |
16 opstack = "val list" |
16 locvars = "val list" |
17 locvars = "val list" |
17 p_count = nat |
18 p_count = nat |
18 |
19 |
19 frame = "opstack \\<times> |
20 frame = "opstack \<times> |
20 locvars \\<times> |
21 locvars \<times> |
21 cname \\<times> |
22 cname \<times> |
22 sig \\<times> |
23 sig \<times> |
23 p_count" |
24 p_count" |
24 |
25 |
25 (* operand stack *) |
26 (* operand stack *) |
26 (* local variables *) |
27 (* local variables *) |
27 (* name of def. class defined *) |
28 (* name of def. class defined *) |
28 (* meth name+param_desc *) |
29 (* meth name+param_desc *) |
29 (* program counter within frame *) |
30 (* program counter within frame *) |
30 |
31 |
31 |
32 |
32 (** exceptions **) |
33 text {* exceptions: *} |
33 |
|
34 constdefs |
34 constdefs |
35 raise_xcpt :: "bool => xcpt => xcpt option" |
35 raise_xcpt :: "bool => xcpt => xcpt option" |
36 "raise_xcpt c x == (if c then Some x else None)" |
36 "raise_xcpt c x == (if c then Some x else None)" |
37 |
|
38 (** runtime state **) |
|
39 |
|
40 types |
|
41 jvm_state = "xcpt option \\<times> aheap \\<times> frame list" |
|
42 |
37 |
43 |
38 |
|
39 text {* runtime state: *} |
|
40 types |
|
41 jvm_state = "xcpt option \<times> aheap \<times> frame list" |
44 |
42 |
45 (** dynamic method lookup **) |
|
46 |
43 |
|
44 text {* dynamic method lookup: *} |
47 constdefs |
45 constdefs |
48 dyn_class :: "'code prog \\<times> sig \\<times> cname => cname" |
46 dyn_class :: "'code prog \<times> sig \<times> cname => cname" |
49 "dyn_class == \\<lambda>(G,sig,C). fst(the(method(G,C) sig))" |
47 "dyn_class == \<lambda>(G,sig,C). fst(the(method(G,C) sig))" |
|
48 |
50 end |
49 end |