author | kleing |
Mon, 20 Nov 2000 16:37:42 +0100 | |
changeset 10496 | f2d304bdf3cc |
parent 10042 | 7164dc0d24d8 |
child 10592 | fc0b575a2cf7 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/BV/BVSpec.thy |
2 |
ID: $Id$ |
|
3 |
Author: Cornelia Pusch |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
*) |
|
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 | 11 |
|
12 |
constdefs |
|
10042 | 13 |
wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] => bool" |
14 |
"wt_instr i G rT phi max_pc pc == |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
15 |
app i G rT (phi!pc) \<and> |
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 | 18 |
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool" |
19 |
"wt_start G C pTs mxl phi == |
|
10496 | 20 |
G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0" |
8011 | 21 |
|
22 |
||
10042 | 23 |
wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] => bool" |
24 |
"wt_method G C pTs rT mxl ins phi == |
|
8011 | 25 |
let max_pc = length ins |
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> |
10042 | 28 |
(\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi max_pc pc)" |
8011 | 29 |
|
10042 | 30 |
wt_jvm_prog :: "[jvm_prog,prog_type] => bool" |
31 |
"wt_jvm_prog G phi == |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
32 |
wf_prog (\<lambda>G C (sig,rT,maxl,b). |
8011 | 33 |
wt_method G C (snd sig) rT maxl b (phi C sig)) G" |
34 |
||
9559 | 35 |
|
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 | 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 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
41 |
lemma wt_jvm_prog_impl_wt_instr: |
10042 | 42 |
"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins |] |
43 |
==> wt_instr (ins!pc) G rT (phi C sig) (length ins) pc"; |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
44 |
by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
45 |
simp, simp add: wf_mdecl_def wt_method_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
46 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
47 |
lemma wt_jvm_prog_impl_wt_start: |
10042 | 48 |
"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) |] ==> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
49 |
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
|
50 |
by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
51 |
simp, simp add: wf_mdecl_def wt_method_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
52 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
53 |
(* for most instructions wt_instr collapses: *) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
54 |
lemma |
10042 | 55 |
"succs i pc = [pc+1] ==> wt_instr i G rT phi max_pc pc = |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
56 |
(app i G 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
|
57 |
by (simp add: wt_instr_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
58 |
|
8011 | 59 |
end |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
60 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
61 |