src/HOL/MicroJava/BV/BVSpec.thy
author kleing
Sun Dec 16 00:17:44 2001 +0100 (2001-12-16)
changeset 12516 d09d0f160888
parent 11085 b830bf10bf71
child 12911 704713ca07ea
permissions -rw-r--r--
exceptions
nipkow@8011
     1
(*  Title:      HOL/MicroJava/BV/BVSpec.thy
nipkow@8011
     2
    ID:         $Id$
kleing@12516
     3
    Author:     Cornelia Pusch, Gerwin Klein
nipkow@8011
     4
    Copyright   1999 Technische Universitaet Muenchen
nipkow@8011
     5
nipkow@8011
     6
*)
nipkow@8011
     7
kleing@9757
     8
header "The Bytecode Verifier"
kleing@9757
     9
kleing@12516
    10
theory BVSpec = Effect:
kleing@12516
    11
kleing@12516
    12
text {*
kleing@12516
    13
  This theory contains a specification of the BV. The specification
kleing@12516
    14
  describes correct typings of method bodies; it corresponds 
kleing@12516
    15
  to type \emph{checking}.
kleing@12516
    16
*}
nipkow@8011
    17
nipkow@8011
    18
constdefs
kleing@12516
    19
  wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,
kleing@12516
    20
                exception_table,p_count] => bool"
kleing@12516
    21
  "wt_instr i G rT phi mxs max_pc et pc == 
kleing@12516
    22
  app i G mxs rT pc et (phi!pc) \<and>
kleing@12516
    23
  (\<forall>(pc',s') \<in> set (eff i G pc et (phi!pc)). pc' < max_pc \<and> G \<turnstile> s' <=' phi!pc')"
kleing@9549
    24
kleing@12516
    25
  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
kleing@12516
    26
  "wt_start G C pTs mxl phi == 
kleing@12516
    27
  G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
nipkow@8011
    28
kleing@12516
    29
  wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,
kleing@12516
    30
                 exception_table,method_type] => bool"
kleing@12516
    31
  "wt_method G C pTs rT mxs mxl ins et phi ==
kleing@12516
    32
  let max_pc = length ins in
kleing@12516
    33
  0 < max_pc \<and> wt_start G C pTs mxl phi \<and> 
kleing@12516
    34
  (\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc et pc)"
nipkow@8011
    35
kleing@12516
    36
  wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
kleing@12516
    37
  "wt_jvm_prog G phi ==
kleing@12516
    38
  wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)).
kleing@12516
    39
           wt_method G C (snd sig) rT maxs maxl b et (phi C sig)) G"
kleing@9559
    40
kleing@9559
    41
kleing@9549
    42
lemma wt_jvm_progD:
kleing@12516
    43
  "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
kleing@12516
    44
  by (unfold wt_jvm_prog_def, blast)
kleing@9549
    45
oheimb@10629
    46
lemma wt_jvm_prog_impl_wt_instr:
kleing@12516
    47
  "[| wt_jvm_prog G phi; is_class G C;
kleing@12516
    48
      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et); pc < length ins |] 
kleing@12516
    49
  ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) et pc";
kleing@12516
    50
  by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
kleing@12516
    51
      simp, simp, simp add: wf_mdecl_def wt_method_def)
kleing@9549
    52
oheimb@10629
    53
lemma wt_jvm_prog_impl_wt_start:
kleing@12516
    54
  "[| wt_jvm_prog G phi; is_class G C;
kleing@12516
    55
      method (G,C) sig = Some (C,rT,maxs,maxl,ins,et) |] ==> 
kleing@12516
    56
  0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
kleing@12516
    57
  by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
kleing@12516
    58
      simp, simp, simp add: wf_mdecl_def wt_method_def)
kleing@9549
    59
nipkow@8011
    60
end