author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 28524 | 644b62cf678f |
child 35417 | 47ee18b6ae32 |
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 |
|
11 |
consts |
|
10057 | 12 |
exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
13 |
||
8011 | 14 |
|
12519 | 15 |
-- "exec is not recursive. recdef is just used for pattern matching" |
8011 | 16 |
recdef exec "{}" |
10057 | 17 |
"exec (G, xp, hp, []) = None" |
8011 | 18 |
|
10057 | 19 |
"exec (G, None, hp, (stk,loc,C,sig,pc)#frs) = |
9376 | 20 |
(let |
12519 | 21 |
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 |
|
23 |
in Some (find_handler G xcpt' hp' frs'))" |
|
8011 | 24 |
|
10057 | 25 |
"exec (G, Some xp, hp, frs) = None" |
8011 | 26 |
|
27 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset
|
28 |
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
|
29 |
("_ |- _ -jvm-> _" [61,61,61]60) where |
11372 | 30 |
"G |- s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*" |
10057 | 31 |
|
32 |
||
11372 | 33 |
syntax (xsymbols) |
12519 | 34 |
exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" |
13006 | 35 |
("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60) |
8011 | 36 |
|
13052 | 37 |
text {* |
38 |
The start configuration of the JVM: in the start heap, we call a |
|
39 |
method @{text m} of class @{text C} in program @{text G}. The |
|
40 |
@{text this} pointer of the frame is set to @{text Null} to simulate |
|
41 |
a static method invokation. |
|
42 |
*} |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset
|
43 |
definition start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" where |
13052 | 44 |
"start_state G C m \<equiv> |
13056
4fd18d409fd7
workaround for "ins" bug in sml/nj + code generator
kleing
parents:
13052
diff
changeset
|
45 |
let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in |
28524 | 46 |
(None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])" |
13052 | 47 |
|
8011 | 48 |
end |