src/HOL/MicroJava/JVM/JVMInstructions.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/JVMInstructions.thy	Mon Jul 17 14:00:53 2000 +0200
@@ -0,0 +1,36 @@
+(*  Title:      HOL/MicroJava/JVM/JVMInstructions.thy
+    ID:         $Id$
+    Author:     Gerwin Klein
+    Copyright   2000 Technische Universitaet Muenchen
+
+Instructions of the JVM
+*)
+
+JVMInstructions = JVMState +
+
+datatype 
+  instr = Load nat                  (* load from local variable *)
+        | Store nat                 (* store into local variable *)
+        | Bipush int                (* push int *)
+        | Aconst_null               (* push null *)
+        | New cname                 (* create object *)
+        | Getfield vname cname	  	(* Fetch field from object *)
+        | Putfield vname cname		  (* Set field in object     *)
+        | Checkcast cname	          (* Check whether object is of given type *)
+        | Invoke mname "(ty list)"  (* inv. instance meth of an object *)
+        | Return
+        | Pop
+        | Dup
+        | Dup_x1
+        | Dup_x2
+        | Swap
+        | IAdd
+        | Goto int
+        | Ifcmpeq int               (* Branch if int/ref comparison succeeds *)
+
+
+types
+  bytecode = "instr list"
+  jvm_prog = "(nat \\<times> bytecode) prog" 
+
+end