--- a/src/HOL/MicroJava/J/Eval.thy Wed Aug 02 16:49:26 2000 +0200
+++ b/src/HOL/MicroJava/J/Eval.thy Wed Aug 02 17:54:55 2000 +0200
@@ -21,12 +21,12 @@
exec :: "[java_mb prog,xstate,stmt, xstate] \\<Rightarrow> bool "("_\\<turnstile>_ -_\\<rightarrow> _" [51,82,82, 82]81)
translations
- "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" == "(s, e, v, x, s') \\<in> eval G"
- "G\\<turnstile>s -e \\<succ> v\\<rightarrow> s' " == "(s, e, v, s') \\<in> eval G"
- "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" == "(s, e, v, x, s') \\<in> evals G"
- "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> s' " == "(s, e, v, s') \\<in> evals G"
- "G\\<turnstile>s -c \\<rightarrow> (x,s')" == "(s, c, x, s') \\<in> exec G"
- "G\\<turnstile>s -c \\<rightarrow> s' " == "(s, c, s') \\<in> exec G"
+ "G\\<turnstile>s -e \\<succ> v\\<rightarrow> (x,s')" <= "(s, e, v, (_args x s')) \\<in> eval G"
+ "G\\<turnstile>s -e \\<succ> v\\<rightarrow> s' " == "(s, e, v, s' ) \\<in> eval G"
+ "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> (x,s')" <= "(s, e, v, (_args x s')) \\<in> evals G"
+ "G\\<turnstile>s -e[\\<succ>]v\\<rightarrow> s' " == "(s, e, v, s' ) \\<in> evals G"
+ "G\\<turnstile>s -c \\<rightarrow> (x,s')" <= "(s, c, (_args x s')) \\<in> exec G"
+ "G\\<turnstile>s -c \\<rightarrow> s' " == "(s, c, s') \\<in> exec G"
inductive "eval G" "evals G" "exec G" intrs
@@ -49,7 +49,7 @@
Lit "G\\<turnstile>Norm s -Lit v\\<succ>v\\<rightarrow> Norm s"
BinOp "\\<lbrakk>G\\<turnstile>Norm s -e1\\<succ>v1\\<rightarrow> s1;
- G\\<turnstile>s1 -e1\\<succ>v2\\<rightarrow> s2;
+ G\\<turnstile>s1 -e2\\<succ>v2\\<rightarrow> s2;
v = (case bop of Eq \\<Rightarrow> Bool (v1 = v2)
| Add \\<Rightarrow> Intg (the_Intg v1 + the_Intg v2))\\<rbrakk> \\<Longrightarrow>
G\\<turnstile>Norm s -BinOp bop e1 e2\\<succ>v\\<rightarrow> s2"
--- a/src/HOL/MicroJava/J/Example.thy Wed Aug 02 16:49:26 2000 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Wed Aug 02 17:54:55 2000 +0200
@@ -22,10 +22,8 @@
class Example {
public static void main (String args[]) {
- Base e;
- e=new Ext();
- try {e.foo(null); }
- catch (NullPointerException x) {}
+ Base e=new Ext();
+ e.foo(null);
}
}
*)
@@ -91,12 +89,6 @@
Expr(LAcc e..foo({[Class Base]}[Lit Null]))"
-
-
-
-
-
-
syntax
NP :: xcpt
@@ -106,7 +98,7 @@
translations
- "NP" == "NullPointer"
+ "NP" == "NullPointer"
"tprg" == "[ObjectC, BaseC, ExtC]"
"obj1" <= "(Ext, empty((vee, Base)\\<mapsto>Bool False)
((vee, Ext )\\<mapsto>Intg #0))"