author | haftmann |
Tue, 07 Oct 2008 16:07:50 +0200 | |
changeset 28524 | 644b62cf678f |
parent 16417 | 9bc16273c2d4 |
child 35355 | 613e133966ea |
child 35416 | d8d7d1b785af |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/JVM/JVMExec.thy |
2 |
ID: $Id$ |
|
12519 | 3 |
Author: Cornelia Pusch, Gerwin Klein |
8011 | 4 |
Copyright 1999 Technische Universitaet Muenchen |
5 |
*) |
|
6 |
||
12911 | 7 |
header {* \isaheader{Program Execution in the JVM} *} |
10057 | 8 |
|
16417 | 9 |
theory JVMExec imports JVMExecInstr JVMExceptions begin |
10057 | 10 |
|
8011 | 11 |
|
12 |
consts |
|
10057 | 13 |
exec :: "jvm_prog \<times> jvm_state => jvm_state option" |
14 |
||
8011 | 15 |
|
12519 | 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 |
12519 | 22 |
i = fst(snd(snd(snd(snd(the(method (G,C) sig)))))) ! pc; |
23 |
(xcpt', hp', frs') = exec_instr i G hp stk loc C sig pc frs |
|
24 |
in Some (find_handler G xcpt' hp' frs'))" |
|
8011 | 25 |
|
10057 | 26 |
"exec (G, Some xp, hp, frs) = None" |
8011 | 27 |
|
28 |
||
29 |
constdefs |
|
12519 | 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) |
12519 | 36 |
exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" |
13006 | 37 |
("_ \<turnstile> _ -jvm\<rightarrow> _" [61,61,61]60) |
8011 | 38 |
|
13052 | 39 |
text {* |
40 |
The start configuration of the JVM: in the start heap, we call a |
|
41 |
method @{text m} of class @{text C} in program @{text G}. The |
|
42 |
@{text this} pointer of the frame is set to @{text Null} to simulate |
|
43 |
a static method invokation. |
|
44 |
*} |
|
45 |
constdefs |
|
46 |
start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" |
|
47 |
"start_state G C m \<equiv> |
|
13056
4fd18d409fd7
workaround for "ins" bug in sml/nj + code generator
kleing
parents:
13052
diff
changeset
|
48 |
let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in |
28524 | 49 |
(None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])" |
13052 | 50 |
|
8011 | 51 |
end |