--- /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