author | krauss |
Tue, 02 Mar 2010 12:26:50 +0100 | |
changeset 35440 | bdf8ad377877 |
parent 35417 | 47ee18b6ae32 |
child 53024 | e0968e1f6fe9 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/JVM/JVMExec.thy |
12519 | 2 |
Author: Cornelia Pusch, Gerwin Klein |
8011 | 3 |
Copyright 1999 Technische Universitaet Muenchen |
4 |
*) |
|
5 |
||
12911 | 6 |
header {* \isaheader{Program Execution in the JVM} *} |
10057 | 7 |
|
16417 | 8 |
theory JVMExec imports JVMExecInstr JVMExceptions begin |
10057 | 9 |
|
8011 | 10 |
|
35440 | 11 |
fun |
10057 | 12 |
exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
35440 | 13 |
-- "exec is not recursive. fun is just used for pattern matching" |
14 |
where |
|
10057 | 15 |
"exec (G, xp, hp, []) = None" |
8011 | 16 |
|
35440 | 17 |
| "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
9376 | 18 |
(let |
12519 | 19 |
i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc; |
20 |
(xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs |
|
21 |
in Some (find_handler G xcpt' hp' frs'))" |
|
8011 | 22 |
|
35440 | 23 |
| "exec (G, Some xp, hp, frs) = None" |
8011 | 24 |
|
25 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset
|
26 |
definition exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset
|
27 |
("_ |- _ -jvm-> _" [61,61,61]60) where |
11372 | 28 |
"G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*" |
10057 | 29 |
|
30 |
||
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
28524
diff
changeset
|
31 |
notation (xsymbols) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
28524
diff
changeset
|
32 |
exec_all ("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60) |
8011 | 33 |
|
13052 | 34 |
text {* |
35 |
The start configuration of the JVM: in the start heap, we call a |
|
36 |
method @{text m} of class @{text C} in program @{text G}. The |
|
37 |
@{text this} pointer of the frame is set to @{text Null} to simulate |
|
38 |
a static method invokation. |
|
39 |
*} |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset
|
40 |
definition start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" where |
13052 | 41 |
"start_state G C m \<equiv> |
13056
4fd18d409fd7
workaround for "ins" bug in sml/nj + code generator
kleing
parents:
13052
diff
changeset
|
42 |
let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in |
28524 | 43 |
(None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])" |
13052 | 44 |
|
8011 | 45 |
end |