src/HOL/MicroJava/BV/LBVCorrect.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Tue Feb 15 17:51:11 2000 +0100
@@ -0,0 +1,28 @@
+(*  Title:      HOL/MicroJava/BV/BVLcorrect.thy
+    ID:         $Id$
+    Author:     Gerwin Klein
+    Copyright   1999 Technische Universitaet Muenchen
+
+    Correctness of the lightweight bytecode verifier
+*)
+
+LBVCorrect = LBVSpec +
+
+constdefs
+fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
+"fits phi is G rT s0 s2 cert \\<equiv> (\\<forall> a b i s1. (a@(i#b) = is) \\<longrightarrow> 
+                   wtl_inst_list a G rT s0 s1 cert (length is) 0 \\<longrightarrow> 
+                   wtl_inst_list (i#b) G rT s1 s2 cert (length is) (length a) \\<longrightarrow> 
+                      ((cert!(length a) = None \\<longrightarrow> phi!(length a) = s1) \\<and> 
+                      (\\<forall> t. cert!(length a) = Some t \\<longrightarrow> phi!(length a) = t)))"
+
+
+fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool" 
+"fits_partial phi pc is G rT s0 s2 cert \\<equiv> (\\<forall> a b i s1. (a@(i#b) = is) \\<longrightarrow> 
+                   wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \\<longrightarrow> 
+                   wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \\<longrightarrow> 
+                      ((cert!(pc+length a) = None \\<longrightarrow> phi!(pc+length a) = s1) \\<and> 
+                      (\\<forall> t. cert!(pc+length a) = Some t \\<longrightarrow> phi!(pc+length a) = t)))"
+  
+  
+end