1 (* Title: HOL/MicroJava/JVM/JVMExec.thy |
1 (* Title: HOL/MicroJava/JVM/JVMExec.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 Execution of the JVM |
|
7 *) |
5 *) |
8 |
6 |
9 JVMExec = JVMExecInstr + |
7 header {* Program Execution in the JVM *} |
|
8 |
|
9 theory JVMExec = JVMExecInstr : |
|
10 |
10 |
11 |
11 consts |
12 consts |
12 exec :: "jvm_prog \\<times> jvm_state => jvm_state option" |
13 exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
|
14 |
13 |
15 |
14 (** exec is not recursive. recdef is just used for pattern matching **) |
16 (** exec is not recursive. recdef is just used for pattern matching **) |
15 recdef exec "{}" |
17 recdef exec "{}" |
16 "exec (G, xp, hp, []) = None" |
18 "exec (G, xp, hp, []) = None" |
17 |
19 |
18 "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
20 "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
19 (let |
21 (let |
20 i = snd(snd(snd(the(method (G,C) sig)))) ! pc |
22 i = snd(snd(snd(the(method (G,C) sig)))) ! pc |
21 in |
23 in |
22 Some (exec_instr i G hp stk loc C sig pc frs))" |
24 Some (exec_instr i G hp stk loc C sig pc frs))" |
23 |
25 |
24 "exec (G, Some xp, hp, frs) = None" |
26 "exec (G, Some xp, hp, frs) = None" |
25 |
27 |
26 |
28 |
27 constdefs |
29 constdefs |
28 exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" ("_ \\<turnstile> _ -jvm-> _" [61,61,61]60) |
30 exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" |
29 "G \\<turnstile> s -jvm-> t == (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*" |
31 ("_ \<turnstile> _ -jvm-> _" [61,61,61]60) |
|
32 "G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*" |
|
33 |
|
34 |
|
35 syntax (HTML output) |
|
36 exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" |
|
37 ("_ |- _ -jvm-> _" [61,61,61]60) |
30 |
38 |
31 end |
39 end |