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