6 header {* \isaheader{Program Execution in the JVM} *} |
6 header {* \isaheader{Program Execution in the JVM} *} |
7 |
7 |
8 theory JVMExec imports JVMExecInstr JVMExceptions begin |
8 theory JVMExec imports JVMExecInstr JVMExceptions begin |
9 |
9 |
10 |
10 |
11 consts |
11 fun |
12 exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
12 exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
13 |
13 -- "exec is not recursive. fun is just used for pattern matching" |
14 |
14 where |
15 -- "exec is not recursive. recdef is just used for pattern matching" |
|
16 recdef exec "{}" |
|
17 "exec (G, xp, hp, []) = None" |
15 "exec (G, xp, hp, []) = None" |
18 |
16 |
19 "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
17 | "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
20 (let |
18 (let |
21 i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc; |
19 i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc; |
22 (xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs |
20 (xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs |
23 in Some (find_handler G xcpt' hp' frs'))" |
21 in Some (find_handler G xcpt' hp' frs'))" |
24 |
22 |
25 "exec (G, Some xp, hp, frs) = None" |
23 | "exec (G, Some xp, hp, frs) = None" |
26 |
24 |
27 |
25 |
28 definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" |
26 definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" |
29 ("_ |- _ -jvm-> _" [61,61,61]60) where |
27 ("_ |- _ -jvm-> _" [61,61,61]60) where |
30 "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*" |
28 "G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*" |