Up to index of Isabelle/HOL/arrays
theory BVSpec = Effect:(* Title: HOL/MicroJava/BV/BVSpec.thy
ID: $Id: BVSpec.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
Author: Cornelia Pusch, Gerwin Klein
Copyright 1999 Technische Universitaet Muenchen
*)
header {* \isaheader{The Bytecode Verifier}\label{sec:BVSpec} *}
theory BVSpec = Effect:
text {*
This theory contains a specification of the BV. The specification
describes correct typings of method bodies; it corresponds
to type \emph{checking}.
*}
constdefs
-- "The method type only contains declared classes:"
check_types :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> state list \<Rightarrow> bool"
"check_types G mxs mxr mpc phi \<equiv> set phi \<subseteq> states G mxs mxr mpc"
-- "An instruction is welltyped if it is applicable and its effect"
-- "is compatible with the type at all successor instructions:"
wt_instr :: "[instr,jvm_prog,cname,ty,method_type,nat,bool,
p_count,exception_table,p_count] \<Rightarrow> bool"
"wt_instr i G C rT phi mxs ini max_pc et pc \<equiv>
app i G C pc mxs max_pc rT ini et (phi!pc) \<and>
(\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> s' \<subseteq> phi!pc')"
-- {* The type at @{text "pc=0"} conforms to the method calling convention: *}
wt_start :: "[jvm_prog,cname,mname,ty list,nat,method_type] \<Rightarrow> bool"
"wt_start G C mn pTs mxl phi \<equiv>
let
this = OK (if mn = init \<and> C \<noteq> Object then PartInit C else Init (Class C));
start = (([],this#(map OK (map Init pTs))@(replicate mxl Err)),C=Object)
in
start \<in> phi!0"
-- "A method is welltyped if the body is not empty, if execution does not"
-- "leave the body, if the method type covers all instructions and mentions"
-- "declared classes only, if the method calling convention is respected, and"
-- "if all instructions are welltyped."
wt_method :: "[jvm_prog,cname,mname,ty list,ty,nat,nat,
instr list,exception_table,method_type] \<Rightarrow> bool"
"wt_method G C mn pTs rT mxs mxl ins et phi \<equiv>
let max_pc = length ins in
0 < max_pc \<and>
length phi = length ins \<and>
check_types G mxs (1+length pTs+mxl) max_pc (map OK phi) \<and>
wt_start G C mn pTs mxl phi \<and>
(\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins!pc) G C rT phi mxs (mn=init) max_pc et pc)"
wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool"
"wt_jvm_prog G phi \<equiv>
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
wt_method G C (fst sig) (snd sig) rT maxs maxl b et (phi C sig)) G"
lemma wt_jvm_progD:
"wt_jvm_prog G phi \<Longrightarrow> (\<exists>wt. wf_prog wt G)"
by (unfold wt_jvm_prog_def, blast)
lemma wt_jvm_prog_impl_wt_instr:
"\<lbrakk> wt_jvm_prog G phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins \<rbrakk>
\<Longrightarrow> wt_instr (ins!pc) G C rT (phi C sig) maxs (fst sig=init) (length ins) et pc";
by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
lemma wt_jvm_prog_impl_wt_start:
"\<lbrakk> wt_jvm_prog G phi; is_class G C;
method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) \<rbrakk> \<Longrightarrow>
0 < (length ins) \<and> wt_start G C (fst sig) (snd sig) maxl (phi C sig)"
by (unfold wt_jvm_prog_def, drule method_wf_mdecl,
simp, simp, simp add: wf_mdecl_def wt_method_def)
end
lemma wt_jvm_progD:
wt_jvm_prog G phi ==> EX wt. wf_prog wt G
lemma wt_jvm_prog_impl_wt_instr:
[| wt_jvm_prog G phi; is_class G C;
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et); pc < length ins |]
==> wt_instr (ins ! pc) G C rT (phi C sig) maxs (fst sig = init) (length ins) et
pc
lemma wt_jvm_prog_impl_wt_start:
[| wt_jvm_prog G phi; is_class G C;
method (G, C) sig = Some (C, rT, maxs, maxl, ins, et) |]
==> 0 < length ins & wt_start G C (fst sig) (snd sig) maxl (phi C sig)