author | wenzelm |
Tue, 16 Jan 2018 09:30:00 +0100 | |
changeset 67443 | 3abf6a722518 |
parent 62042 | 6c6ccf573479 |
child 67613 | ce654b0e6d69 |
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 |
||
61361 | 6 |
section \<open>Program Execution in the JVM\<close> |
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" |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
62042
diff
changeset
|
13 |
\<comment> \<open>exec is not recursive. fun is just used for pattern matching\<close> |
35440 | 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" |
53024 | 27 |
("_ \<turnstile> _ \<midarrow>jvm\<rightarrow> _" [61,61,61]60) where |
28 |
"G \<turnstile> s \<midarrow>jvm\<rightarrow> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*" |
|
10057 | 29 |
|
30 |
||
61361 | 31 |
text \<open> |
13052 | 32 |
The start configuration of the JVM: in the start heap, we call a |
62042 | 33 |
method \<open>m\<close> of class \<open>C\<close> in program \<open>G\<close>. The |
34 |
\<open>this\<close> pointer of the frame is set to \<open>Null\<close> to simulate |
|
13052 | 35 |
a static method invokation. |
61361 | 36 |
\<close> |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
28524
diff
changeset
|
37 |
definition start_state :: "jvm_prog \<Rightarrow> cname \<Rightarrow> mname \<Rightarrow> jvm_state" where |
13052 | 38 |
"start_state G C m \<equiv> |
13056
4fd18d409fd7
workaround for "ins" bug in sml/nj + code generator
kleing
parents:
13052
diff
changeset
|
39 |
let (C',rT,mxs,mxl,i,et) = the (method (G,C) (m,[])) in |
28524 | 40 |
(None, start_heap G, [([], Null # replicate mxl undefined, C, (m,[]), 0)])" |
13052 | 41 |
|
8011 | 42 |
end |