Theory BVSpec

Up to index of Isabelle/HOL/verificard

(*  Title:      HOL/MicroJava/BV/BVSpec.thy
    ID:         $Id: BVSpec.thy,v 1.21.2.14 2002/03/09 22:12:50 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

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 rT ini et (phi!pc) \<and>
  (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"

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 = Some (([],this#(map OK (map Init pTs))@(replicate mxl Err)),C=Object)
  in
    G \<turnstile> start <=' phi!0"

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