src/HOL/MicroJava/BV/BVSpec.thy
author oheimb
Thu, 07 Dec 2000 17:59:24 +0100
changeset 10629 d790faef9c07
parent 10612 779af7c58743
child 10638 17063aee1d86
permissions -rw-r--r--
removed two intermediate comments
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/MicroJava/BV/BVSpec.thy
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     3
    Author:     Cornelia Pusch
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     4
    Copyright   1999 Technische Universitaet Muenchen
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     5
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     6
*)
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
     7
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 9559
diff changeset
     8
header "The Bytecode Verifier"
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 9559
diff changeset
     9
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 9559
diff changeset
    10
theory BVSpec = Step:
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    11
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    12
constdefs
10592
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    13
wt_instr :: "[instr,jvm_prog,ty,method_type,nat,p_count,p_count] => bool"
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    14
"wt_instr i G rT phi mxs max_pc pc == 
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    15
    app i G mxs rT (phi!pc) \<and>
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 9559
diff changeset
    16
   (\<forall> pc' \<in> set (succs i pc). pc' < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!pc'))"
9549
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    17
10042
7164dc0d24d8 unsymbolized
kleing
parents: 9757
diff changeset
    18
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
7164dc0d24d8 unsymbolized
kleing
parents: 9757
diff changeset
    19
"wt_start G C pTs mxl phi == 
10496
f2d304bdf3cc BCV integration (first step)
kleing
parents: 10042
diff changeset
    20
    G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    21
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    22
10592
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    23
wt_method :: "[jvm_prog,cname,ty list,ty,nat,nat,instr list,method_type] => bool"
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    24
"wt_method G C pTs rT mxs mxl ins phi ==
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    25
	let max_pc = length ins
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    26
        in
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 9559
diff changeset
    27
	0 < max_pc \<and> wt_start G C pTs mxl phi \<and> 
10592
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    28
	(\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi mxs max_pc pc)"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    29
10042
7164dc0d24d8 unsymbolized
kleing
parents: 9757
diff changeset
    30
wt_jvm_prog :: "[jvm_prog,prog_type] => bool"
7164dc0d24d8 unsymbolized
kleing
parents: 9757
diff changeset
    31
"wt_jvm_prog G phi ==
10592
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    32
   wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b)).
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    33
              wt_method G C (snd sig) rT maxs maxl b (phi C sig)) G"
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    34
9559
kleing
parents: 9549
diff changeset
    35
kleing
parents: 9549
diff changeset
    36
9549
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    37
lemma wt_jvm_progD:
10042
7164dc0d24d8 unsymbolized
kleing
parents: 9757
diff changeset
    38
"wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)"
9549
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    39
by (unfold wt_jvm_prog_def, blast)
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    40
10629
d790faef9c07 removed two intermediate comments
oheimb
parents: 10612
diff changeset
    41
lemma wt_jvm_prog_impl_wt_instr:
10612
779af7c58743 improved superclass entry for classes and definition status of is_class, class
oheimb
parents: 10593
diff changeset
    42
"[| wt_jvm_prog G phi; is_class G C;
779af7c58743 improved superclass entry for classes and definition status of is_class, class
oheimb
parents: 10593
diff changeset
    43
    method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] 
10592
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    44
 ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc";
9549
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    45
by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
10612
779af7c58743 improved superclass entry for classes and definition status of is_class, class
oheimb
parents: 10593
diff changeset
    46
    simp, simp, simp add: wf_mdecl_def wt_method_def)
9549
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    47
10629
d790faef9c07 removed two intermediate comments
oheimb
parents: 10612
diff changeset
    48
lemma wt_jvm_prog_impl_wt_start:
10612
779af7c58743 improved superclass entry for classes and definition status of is_class, class
oheimb
parents: 10593
diff changeset
    49
"[| wt_jvm_prog G phi; is_class G C;
779af7c58743 improved superclass entry for classes and definition status of is_class, class
oheimb
parents: 10593
diff changeset
    50
    method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> 
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 9559
diff changeset
    51
 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)"
9549
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    52
by (unfold wt_jvm_prog_def, drule method_wf_mdecl, 
10612
779af7c58743 improved superclass entry for classes and definition status of is_class, class
oheimb
parents: 10593
diff changeset
    53
    simp, simp, simp add: wf_mdecl_def wt_method_def)
9549
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    54
10593
3288024b4d43 fixed document preparation
kleing
parents: 10592
diff changeset
    55
text {* for most instructions wt\_instr collapses: *}
9757
1024a2d80ac0 functional LBV style, dead code, type safety -> Isar
kleing
parents: 9559
diff changeset
    56
lemma  
10592
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    57
"succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = 
fc0b575a2cf7 BCV Integration
kleing
parents: 10496
diff changeset
    58
 (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))"
9549
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    59
by (simp add: wt_instr_def) 
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    60
8011
d14c4e9e9c8e *** empty log message ***
nipkow
parents:
diff changeset
    61
end
9549
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    62
40d64cb4f4e6 BV and LBV specified in terms of app and step functions
kleing
parents: 9376
diff changeset
    63