| author | oheimb |
| Tue, 12 Jun 2001 14:11:00 +0200 | |
| changeset 11372 | 648795477bb5 |
| parent 11177 | 749fd046002f |
| child 12519 | a955fe2879ba |
| 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 |
||
| 10057 | 7 |
|
8 |
header {* State of the JVM *}
|
|
| 8011 | 9 |
|
10 |
||
|
10922
f1209aff9517
Store.thy is obsolete (newref isn't used any more)
kleing
parents:
10057
diff
changeset
|
11 |
theory JVMState = Conform: |
| 8011 | 12 |
|
| 10057 | 13 |
|
14 |
text {* frame stack :*}
|
|
| 8011 | 15 |
types |
16 |
opstack = "val list" |
|
17 |
locvars = "val list" |
|
18 |
p_count = nat |
|
19 |
||
| 10057 | 20 |
frame = "opstack \<times> |
21 |
locvars \<times> |
|
22 |
cname \<times> |
|
23 |
sig \<times> |
|
24 |
p_count" |
|
| 8011 | 25 |
|
26 |
(* operand stack *) |
|
27 |
(* local variables *) |
|
28 |
(* name of def. class defined *) |
|
29 |
(* meth name+param_desc *) |
|
30 |
(* program counter within frame *) |
|
31 |
||
32 |
||
| 10057 | 33 |
text {* exceptions: *}
|
| 8011 | 34 |
constdefs |
| 10057 | 35 |
raise_xcpt :: "bool => xcpt => xcpt option" |
36 |
"raise_xcpt c x == (if c then Some x else None)" |
|
| 8011 | 37 |
|
38 |
||
| 10057 | 39 |
text {* runtime state: *}
|
40 |
types |
|
41 |
jvm_state = "xcpt option \<times> aheap \<times> frame list" |
|
| 8011 | 42 |
|
43 |
end |