19 evals:: "[java_mb prog,xstate,expr list, |
19 evals:: "[java_mb prog,xstate,expr list, |
20 val list,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_[\\<succ>]_\\<rightarrow> _"[51,82,51,51,82]81) |
20 val list,xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_[\\<succ>]_\\<rightarrow> _"[51,82,51,51,82]81) |
21 exec :: "[java_mb prog,xstate,stmt, xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _" [51,82,82, 82]81) |
21 exec :: "[java_mb prog,xstate,stmt, xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _" [51,82,82, 82]81) |
22 |
22 |
23 translations |
23 translations |
24 "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" <= "(s, e, v, (_args x s')) \\<in> eval G" |
24 "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" <= "(s, e, v, x, s') \\<in> eval G" |
25 "G\\<turnstile>s -e \\<succ> v\\<rightarrow> s' " == "(s, e, v, s' ) \\<in> eval G" |
25 "G\\<turnstile>s -e \\<succ> v\\<rightarrow> s' " == "(s, e, v, s' ) \\<in> eval G" |
26 "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" <= "(s, e, v, (_args x s')) \\<in> evals G" |
26 "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" <= "(s, e, v, x, s') \\<in> evals G" |
27 "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> s' " == "(s, e, v, s' ) \\<in> evals G" |
27 "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> s' " == "(s, e, v, s' ) \\<in> evals G" |
28 "G\\<turnstile>s -c \\<rightarrow> (x,s')" <= "(s, c, (_args x s')) \\<in> exec G" |
28 "G\\<turnstile>s -c \\<rightarrow> (x,s')" <= "(s, c, x, s') \\<in> exec G" |
29 "G\\<turnstile>s -c \\<rightarrow> s' " == "(s, c, s') \\<in> exec G" |
29 "G\\<turnstile>s -c \\<rightarrow> s' " == "(s, c, s') \\<in> exec G" |
30 |
30 |
31 inductive "eval G" "evals G" "exec G" intrs |
31 inductive "eval G" "evals G" "exec G" intrs |
32 |
32 |
33 (* evaluation of expressions *) |
33 (* evaluation of expressions *) |
34 |
34 |