diff -r 69032a618aa9 -r d14c4e9e9c8e src/HOL/MicroJava/BV/BVSpec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Thu Nov 11 12:23:45 1999 +0100
@@ -0,0 +1,201 @@
+(*  Title:      HOL/MicroJava/BV/BVSpec.thy
+    ID:         $Id$
+    Author:     Cornelia Pusch
+    Copyright   1999 Technische Universitaet Muenchen
+
+Specification of bytecode verifier
+*)
+
+BVSpec = Convert +
+
+types
+ method_type 	= "state_type list"
+ class_type	= "sig \\<Rightarrow> method_type"
+ prog_type	= "cname \\<Rightarrow> class_type"
+
+consts
+ wt_LS	:: "[load_and_store,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool"
+primrec
+"wt_LS (Load idx) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 idx < length LT \\<and>
+	 (\\<exists>ts. (LT ! idx) = Some ts \\<and> 
+	       G \\<turnstile> phi ! (pc+1) >>>= (ts # ST , LT)))"
+
+"wt_LS (Store idx) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 idx < length LT \\<and>
+	 (\\<exists>ts ST'. ST = ts # ST' \\<and>
+		   G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT[idx:=Some ts])))"
+
+"wt_LS (Bipush i) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 G \\<turnstile> phi ! (pc+1) >>>= ((PrimT Integer) # ST , LT))"
+
+"wt_LS (Aconst_null) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 G \\<turnstile> phi ! (pc+1) >>>= (NT # ST , LT))"
+
+consts
+ wt_MO	:: "[manipulate_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wt_MO (Getfield F C) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 is_class G C \\<and>
+	 (\\<exists>T oT ST'. cfield (G,C) F = Some(C,T) \\<and>
+                       ST = oT # ST' \\<and> 
+		       G \\<turnstile> oT \\<preceq> (Class C) \\<and>
+		       G \\<turnstile> phi ! (pc+1) >>>= (T # ST' , LT)))"
+
+"wt_MO (Putfield F C) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 is_class G C \\<and> 
+	 (\\<exists>T vT oT ST'.
+             cfield (G,C) F = Some(C,T) \\<and>
+             ST = vT # oT # ST' \\<and> 
+             G \\<turnstile> oT \\<preceq> (Class C) \\<and>
+	     G \\<turnstile> vT \\<preceq> T  \\<and>
+             G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT)))"
+
+
+consts 
+ wt_CO	:: "[create_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wt_CO (New C) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 is_class G C \\<and>
+	 G \\<turnstile> phi ! (pc+1) >>>= ((Class C) # ST , LT))"
+
+consts
+ wt_CH	:: "[check_object,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wt_CH (Checkcast C) G phi max_pc pc = 
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 is_class G C \\<and> 
+	 (\\<exists>rt ST'. ST = RefT rt # ST' \\<and>
+                   G \\<turnstile> phi ! (pc+1) >>>= (Class C # ST' , LT)))"
+
+consts 
+ wt_OS	:: "[op_stack,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wt_OS Pop G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 \\<exists>ts ST'. pc+1 < max_pc \\<and>
+		ST = ts # ST' \\<and> 	 
+		G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT))"
+
+"wt_OS Dup G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 (\\<exists>ts ST'. ST = ts # ST' \\<and> 	 
+		   G \\<turnstile> phi ! (pc+1) >>>= (ts # ts # ST' , LT)))"
+
+"wt_OS Dup_x1 G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 (\\<exists>ts1 ts2 ST'. ST = ts1 # ts2 # ST' \\<and> 	 
+		   G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts1 # ST' , LT)))"
+
+"wt_OS Dup_x2 G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 (\\<exists>ts1 ts2 ts3 ST'. ST = ts1 # ts2 # ts3 # ST' \\<and> 	 
+		   G \\<turnstile> phi ! (pc+1) >>>= (ts1 # ts2 # ts3 # ts1 # ST' , LT)))"
+
+"wt_OS Swap G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and>
+	 (\\<exists>ts ts' ST'. ST = ts' # ts # ST' \\<and> 	 
+		       G \\<turnstile> phi ! (pc+1) >>>= (ts # ts' # ST' , LT)))"
+
+consts 
+ wt_BR	:: "[branch,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wt_BR (Ifcmpeq branch) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 pc+1 < max_pc \\<and> (nat(int pc+branch)) < max_pc \\<and> 
+	 (\\<exists>ts ts' ST'. ST = ts # ts' # ST' \\<and>  ts = ts' \\<and>
+		       G \\<turnstile> phi ! (pc+1) >>>= (ST' , LT) \\<and>
+		       G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST' , LT)))"
+"wt_BR (Goto branch) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+	 (nat(int pc+branch)) < max_pc \\<and> 
+	 G \\<turnstile> phi ! (nat(int pc+branch)) >>>= (ST , LT))"
+
+consts
+ wt_MI :: "[meth_inv,jvm_prog,method_type,p_count,p_count] \\<Rightarrow> bool" 
+primrec
+"wt_MI (Invokevirtual mn fpTs) G phi max_pc pc =
+	(let (ST,LT) = phi ! pc
+	 in
+         pc+1 < max_pc \\<and>
+         (\\<exists>apTs C ST'. ST = (rev apTs) @ (Class C # ST') \\<and>
+         length apTs = length fpTs \\<and>
+         (\\<forall>(aT,fT)\\<in>set(zip apTs fpTs). G \\<turnstile> aT \\<preceq> fT) \\<and>
+         (\\<exists>D rT b. cmethd (G,C) (mn,fpTs) = Some(D,rT,b) \\<and>
+         G \\<turnstile> phi ! (pc+1) >>>= (rT # ST' , LT))))"
+
+constdefs
+ wt_MR	:: "[jvm_prog,ty,method_type,p_count] \\<Rightarrow> bool"
+"wt_MR G rT phi pc \\<equiv>
+	(let (ST,LT) = phi ! pc
+	 in
+	 (\\<exists>T ST'. ST = T # ST' \\<and> G \\<turnstile> T \\<preceq> rT))"
+
+
+constdefs
+ wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count] \\<Rightarrow> bool"
+ "wt_instr instr G rT phi max_pc pc \\<equiv>
+	case instr of
+	  LS ins \\<Rightarrow> wt_LS ins G phi max_pc pc
+	| CO  ins \\<Rightarrow> wt_CO ins G phi max_pc pc
+	| MO  ins \\<Rightarrow> wt_MO ins G phi max_pc pc
+	| CH  ins \\<Rightarrow> wt_CH ins G phi max_pc pc
+	| MI  ins \\<Rightarrow> wt_MI ins G phi max_pc pc
+	| MR      \\<Rightarrow> wt_MR     G rT phi pc
+	| OS  ins \\<Rightarrow> wt_OS ins G phi max_pc pc
+	| BR  ins \\<Rightarrow> wt_BR ins G phi max_pc pc"
+
+
+constdefs
+ wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \\<Rightarrow> bool"
+ "wt_start G C pTs mxl phi \\<equiv> 
+    G \\<turnstile> phi!0 >>>= ([],(Some(Class C))#((map Some pTs))@(replicate mxl None))"
+
+
+ wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \\<Rightarrow> bool"
+ "wt_method G cn pTs rT mxl ins phi \\<equiv>
+	let max_pc = length ins
+        in
+	0 < max_pc \\<and> wt_start G cn pTs mxl phi \\<and> 
+	(\\<forall>pc. pc<max_pc \\<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)"
+
+ wt_jvm_prog :: "[jvm_prog,prog_type] \\<Rightarrow> bool"
+"wt_jvm_prog G phi \\<equiv>
+   wf_prog (\\<lambda>G C (sig,rT,maxl,b).
+              wt_method G C (snd sig) rT maxl b (phi C sig)) G"
+
+end