src/HOL/MicroJava/JVM/Method.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/JVM/Method.thy	Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,41 @@
+(*  Title:      HOL/MicroJava/JVM/Method.thy
+    ID:         $Id$
+    Author:     Cornelia Pusch
+    Copyright   1999 Technische Universitaet Muenchen
+
+Method invocation
+*)
+
+Method = JVMState +
+
+(** method invocation and return instructions **)
+
+datatype 
+ meth_inv = 
+   Invokevirtual   mname (ty list)      (** inv. instance meth of an object **)
+ 
+consts
+ exec_mi :: "[meth_inv,(nat \\<times> 'c)prog,aheap,opstack,p_count] 
+		\\<Rightarrow> (xcpt option \\<times> frame list \\<times> opstack \\<times> p_count)" 
+primrec
+ "exec_mi (Invokevirtual mn ps) G hp stk pc =
+	(let n		= length ps;
+	     argsoref	= take (n+1) stk;
+	     oref	= last argsoref;
+	     xp'	= raise_xcpt (oref=Null) NullPointer;
+	     dynT	= fst(hp \\<And> (the_Addr oref));
+	     (dc,mh,mxl,c)= the (cmethd (G,dynT) (mn,ps));
+	     frs'	= xcpt_update xp' [([],rev argsoref@replicate mxl arbitrary,dc,(mn,ps),0)] []
+	 in
+	 (xp' , frs' , drop (n+1) stk , pc+1))"
+
+
+constdefs
+ exec_mr :: "[opstack,frame list] \\<Rightarrow> frame list"
+"exec_mr stk0 frs \\<equiv>
+	 (let val			= hd stk0;
+	      (stk,loc,cn,met,pc) = hd frs
+	  in
+	  (val#stk,loc,cn,met,pc)#tl frs)"
+
+end