--- a/src/HOL/MicroJava/JVM/JVMExec.thy Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExec.thy Fri Sep 22 13:12:19 2000 +0200
@@ -2,30 +2,38 @@
ID: $Id$
Author: Cornelia Pusch
Copyright 1999 Technische Universitaet Muenchen
-
-Execution of the JVM
*)
-JVMExec = JVMExecInstr +
+header {* Program Execution in the JVM *}
+
+theory JVMExec = JVMExecInstr :
+
consts
- exec :: "jvm_prog \\<times> jvm_state => jvm_state option"
+ exec :: "jvm_prog \<times> jvm_state => jvm_state option"
+
(** exec is not recursive. recdef is just used for pattern matching **)
recdef exec "{}"
- "exec (G, xp, hp, []) = None"
+ "exec (G, xp, hp, []) = None"
- "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
+ "exec (G, None, hp, (stk,loc,C,sig,pc)#frs) =
(let
i = snd(snd(snd(the(method (G,C) sig)))) ! pc
in
Some (exec_instr i G hp stk loc C sig pc frs))"
- "exec (G, Some xp, hp, frs) = None"
+ "exec (G, Some xp, hp, frs) = None"
constdefs
- exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool" ("_ \\<turnstile> _ -jvm-> _" [61,61,61]60)
- "G \\<turnstile> s -jvm-> t == (s,t) \\<in> {(s,t). exec(G,s) = Some t}^*"
+ exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
+ ("_ \<turnstile> _ -jvm-> _" [61,61,61]60)
+ "G \<turnstile> s -jvm-> t == (s,t) \<in> {(s,t). exec(G,s) = Some t}^*"
+
+
+syntax (HTML output)
+ exec_all :: "[jvm_prog,jvm_state,jvm_state] => bool"
+ ("_ |- _ -jvm-> _" [61,61,61]60)
end
--- a/src/HOL/MicroJava/JVM/JVMExecInstr.thy Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMExecInstr.thy Fri Sep 22 13:12:19 2000 +0200
@@ -2,11 +2,14 @@
ID: $Id$
Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
-
-Semantics of JVM instructions
*)
-JVMExecInstr = JVMInstructions + JVMState +
+
+header {* JVM Instruction Semantics *}
+
+
+theory JVMExecInstr = JVMInstructions + JVMState:
+
consts
exec_instr :: "[instr, jvm_prog, aheap, opstack, locvars,
@@ -25,10 +28,10 @@
(None, hp, (Null # stk, vars, Cl, sig, pc+1)#frs)"
"exec_instr (New C) G hp stk vars Cl sig pc frs =
- (let xp' = raise_xcpt (\\<forall>x. hp x \\<noteq> None) OutOfMemory;
+ (let xp' = raise_xcpt (\<forall>x. hp x \<noteq> None) OutOfMemory;
oref = newref hp;
fs = init_vars (fields(G,C));
- hp' = if xp'=None then hp(oref \\<mapsto> (C,fs)) else hp;
+ hp' = if xp'=None then hp(oref \<mapsto> (C,fs)) else hp;
stk' = if xp'=None then (Addr oref)#stk else stk
in
(xp', hp', (stk', vars, Cl, sig, pc+1)#frs))"
@@ -46,13 +49,13 @@
xp' = raise_xcpt (oref=Null) NullPointer;
a = the_Addr oref;
(oc,fs) = the(hp a);
- hp' = if xp'=None then hp(a \\<mapsto> (oc, fs((F,C) \\<mapsto> fval))) else hp
+ hp' = if xp'=None then hp(a \<mapsto> (oc, fs((F,C) \<mapsto> fval))) else hp
in
(xp', hp', (tl (tl stk), vars, Cl, sig, pc+1)#frs))"
"exec_instr (Checkcast C) G hp stk vars Cl sig pc frs =
(let oref = hd stk;
- xp' = raise_xcpt (\\<not> cast_ok G C hp oref) ClassCast;
+ xp' = raise_xcpt (\<not> cast_ok G C hp oref) ClassCast;
stk' = if xp'=None then stk else tl stk
in
(xp', hp, (stk', vars, Cl, sig, pc+1)#frs))"
--- a/src/HOL/MicroJava/JVM/JVMInstructions.thy Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy Fri Sep 22 13:12:19 2000 +0200
@@ -2,11 +2,12 @@
ID: $Id$
Author: Gerwin Klein
Copyright 2000 Technische Universitaet Muenchen
-
-Instructions of the JVM
*)
-JVMInstructions = JVMState +
+header {* Instructions of the JVM *}
+
+
+theory JVMInstructions = JVMState:
datatype
@@ -19,19 +20,19 @@
| Putfield vname cname (* Set field in object *)
| Checkcast cname (* Check whether object is of given type *)
| Invoke cname mname "(ty list)" (* inv. instance meth of an object *)
- | Return
- | Pop
- | Dup
- | Dup_x1
- | Dup_x2
- | Swap
- | IAdd
- | Goto int
+ | Return (* return from method *)
+ | Pop (* pop top element from opstack *)
+ | Dup (* duplicate top element of opstack *)
+ | Dup_x1 (* duplicate next to top element *)
+ | Dup_x2 (* duplicate 3rd element *)
+ | Swap (* swap top and next to top element *)
+ | IAdd (* integer addition *)
+ | Goto int (* goto relative address *)
| Ifcmpeq int (* Branch if int/ref comparison succeeds *)
types
bytecode = "instr list"
- jvm_prog = "(nat \\<times> bytecode) prog"
+ jvm_prog = "(nat \<times> bytecode) prog"
end
--- a/src/HOL/MicroJava/JVM/JVMState.thy Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/JVMState.thy Fri Sep 22 13:12:19 2000 +0200
@@ -2,25 +2,26 @@
ID: $Id$
Author: Cornelia Pusch
Copyright 1999 Technische Universitaet Muenchen
-
-State of the JVM
*)
-JVMState = Store +
+
+header {* State of the JVM *}
-(** frame stack **)
+theory JVMState = Store:
+
+text {* frame stack :*}
types
opstack = "val list"
locvars = "val list"
p_count = nat
- frame = "opstack \\<times>
- locvars \\<times>
- cname \\<times>
- sig \\<times>
- p_count"
+ frame = "opstack \<times>
+ locvars \<times>
+ cname \<times>
+ sig \<times>
+ p_count"
(* operand stack *)
(* local variables *)
@@ -29,22 +30,20 @@
(* program counter within frame *)
-(** exceptions **)
-
+text {* exceptions: *}
constdefs
- raise_xcpt :: "bool => xcpt => xcpt option"
-"raise_xcpt c x == (if c then Some x else None)"
-
-(** runtime state **)
-
-types
- jvm_state = "xcpt option \\<times> aheap \\<times> frame list"
+ raise_xcpt :: "bool => xcpt => xcpt option"
+ "raise_xcpt c x == (if c then Some x else None)"
+text {* runtime state: *}
+types
+ jvm_state = "xcpt option \<times> aheap \<times> frame list"
-(** dynamic method lookup **)
+text {* dynamic method lookup: *}
constdefs
- dyn_class :: "'code prog \\<times> sig \\<times> cname => cname"
-"dyn_class == \\<lambda>(G,sig,C). fst(the(method(G,C) sig))"
+ dyn_class :: "'code prog \<times> sig \<times> cname => cname"
+ "dyn_class == \<lambda>(G,sig,C). fst(the(method(G,C) sig))"
+
end
--- a/src/HOL/MicroJava/JVM/Store.thy Thu Sep 21 19:25:57 2000 +0200
+++ b/src/HOL/MicroJava/JVM/Store.thy Fri Sep 22 13:12:19 2000 +0200
@@ -2,17 +2,25 @@
ID: $Id$
Author: Cornelia Pusch
Copyright 1999 Technische Universitaet Muenchen
-
-The store.
-
-The JVM builds on many notions already defined in Java.
-Conform provides notions for the type safety proof of the Bytecode Verifier.
*)
-Store = Conform +
+header {* Store of the JVM *}
+
+theory Store = Conform:
+
+text {*
+The JVM builds on many notions already defined in Java.
+Conform provides notions for the type safety proof of the Bytecode Verifier.
+*}
+
constdefs
- newref :: "('a \\<leadsto> 'b) => 'a"
+ newref :: "('a \<leadsto> 'b) => 'a"
"newref s == SOME v. s v = None"
+
+lemma newref_None:
+ "hp x = None ==> hp (newref hp) = None"
+by (auto intro: someI2_ex simp add: newref_def)
+
end