author | kleing |
Thu, 21 Sep 2000 10:42:49 +0200 | |
changeset 10042 | 7164dc0d24d8 |
parent 9757 | 1024a2d80ac0 |
child 10496 | f2d304bdf3cc |
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 |
types |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
13 |
method_type = "state_type option list" |
10042 | 14 |
class_type = "sig => method_type" |
15 |
prog_type = "cname => class_type" |
|
8011 | 16 |
|
17 |
constdefs |
|
10042 | 18 |
wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] => bool" |
19 |
"wt_instr i G rT phi max_pc pc == |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
20 |
app i G rT (phi!pc) \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
21 |
(\<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
|
22 |
|
10042 | 23 |
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool" |
24 |
"wt_start G C pTs mxl phi == |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
25 |
G \<turnstile> Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err)) <=' phi!0" |
8011 | 26 |
|
27 |
||
10042 | 28 |
wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] => bool" |
29 |
"wt_method G C pTs rT mxl ins phi == |
|
8011 | 30 |
let max_pc = length ins |
31 |
in |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
32 |
0 < max_pc \<and> wt_start G C pTs mxl phi \<and> |
10042 | 33 |
(\<forall>pc. pc<max_pc --> wt_instr (ins ! pc) G rT phi max_pc pc)" |
8011 | 34 |
|
10042 | 35 |
wt_jvm_prog :: "[jvm_prog,prog_type] => bool" |
36 |
"wt_jvm_prog G phi == |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
37 |
wf_prog (\<lambda>G C (sig,rT,maxl,b). |
8011 | 38 |
wt_method G C (snd sig) rT maxl b (phi C sig)) G" |
39 |
||
9559 | 40 |
|
41 |
||
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
42 |
lemma wt_jvm_progD: |
10042 | 43 |
"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
|
44 |
by (unfold wt_jvm_prog_def, blast) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
45 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
46 |
lemma wt_jvm_prog_impl_wt_instr: |
10042 | 47 |
"[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins |] |
48 |
==> 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
|
49 |
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
|
50 |
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
|
51 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
52 |
lemma wt_jvm_prog_impl_wt_start: |
10042 | 53 |
"[| 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
|
54 |
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
|
55 |
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
|
56 |
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
|
57 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
58 |
(* for most instructions wt_instr collapses: *) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
59 |
lemma |
10042 | 60 |
"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
|
61 |
(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
|
62 |
by (simp add: wt_instr_def) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
63 |
|
8011 | 64 |
end |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
65 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
66 |