| author | wenzelm |
| Sat, 02 Sep 2000 21:49:51 +0200 | |
| changeset 9803 | bc883b390d91 |
| parent 9376 | c32c5696ec2a |
| child 10042 | 7164dc0d24d8 |
| permissions | -rw-r--r-- |
| 8011 | 1 |
(* Title: HOL/MicroJava/JVM/JVMExec.thy |
2 |
ID: $Id$ |
|
3 |
Author: Cornelia Pusch |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
Execution of the JVM |
|
7 |
*) |
|
8 |
||
| 9376 | 9 |
JVMExec = JVMExecInstr + |
| 8011 | 10 |
|
11 |
consts |
|
12 |
exec :: "jvm_prog \\<times> jvm_state \\<Rightarrow> jvm_state option" |
|
13 |
||
| 9376 | 14 |
(** exec is not recursive. recdef is just used for pattern matching **) |
| 8011 | 15 |
recdef exec "{}"
|
16 |
"exec (G, xp, hp, []) = None" |
|
17 |
||
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
18 |
"exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
| 9376 | 19 |
(let |
20 |
i = snd(snd(snd(the(method (G,C) sig)))) ! pc |
|
21 |
in |
|
22 |
Some (exec_instr i G hp stk loc C sig pc frs))" |
|
| 8011 | 23 |
|
| 9376 | 24 |
"exec (G, Some xp, hp, frs) = None" |
| 8011 | 25 |
|
26 |
||
27 |
constdefs |
|
28 |
exec_all :: "[jvm_prog,jvm_state,jvm_state] \\<Rightarrow> bool" ("_ \\<turnstile> _ -jvm\\<rightarrow> _" [61,61,61]60)
|
|
29 |
"G \\<turnstile> s -jvm\\<rightarrow> t \\<equiv> (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
|
|
30 |
||
31 |
end |