|
8245
|
1 |
(* Title: HOL/MicroJava/BV/BVLcorrect.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Gerwin Klein
|
|
|
4 |
Copyright 1999 Technische Universitaet Muenchen
|
|
|
5 |
|
|
|
6 |
Correctness of the lightweight bytecode verifier
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
LBVCorrect = LBVSpec +
|
|
|
10 |
|
|
|
11 |
constdefs
|
|
|
12 |
fits :: "[method_type,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
|
|
8390
|
13 |
"fits phi is G rT s0 s2 cert \\<equiv> fits_partial phi 0 is G rT s0 s2 cert"
|
|
8245
|
14 |
|
|
|
15 |
fits_partial :: "[method_type,nat,instr list,jvm_prog,ty,state_type,state_type,certificate] \\<Rightarrow> bool"
|
|
|
16 |
"fits_partial phi pc is G rT s0 s2 cert \\<equiv> (\\<forall> a b i s1. (a@(i#b) = is) \\<longrightarrow>
|
|
|
17 |
wtl_inst_list a G rT s0 s1 cert (pc+length is) pc \\<longrightarrow>
|
|
|
18 |
wtl_inst_list (i#b) G rT s1 s2 cert (pc+length is) (pc+length a) \\<longrightarrow>
|
|
8390
|
19 |
((cert!(pc+length a) = None \\<longrightarrow> phi!(pc+length a) = s1) \\<and>
|
|
|
20 |
(\\<forall> t. cert!(pc+length a) = Some t \\<longrightarrow> phi!(pc+length a) = t)))"
|
|
8245
|
21 |
|
|
|
22 |
|
|
|
23 |
end
|