author | kleing |
Wed, 30 Aug 2000 21:47:39 +0200 | |
changeset 9757 | 1024a2d80ac0 |
parent 9559 | 1f99296758c2 |
child 10042 | 7164dc0d24d8 |
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" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
14 |
class_type = "sig \<Rightarrow> method_type" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
15 |
prog_type = "cname \<Rightarrow> class_type" |
8011 | 16 |
|
17 |
constdefs |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
18 |
wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] \<Rightarrow> bool" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
19 |
"wt_instr i G rT phi max_pc pc \<equiv> |
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 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
23 |
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] \<Rightarrow> bool" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
24 |
"wt_start G C pTs mxl phi \<equiv> |
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 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
28 |
wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] \<Rightarrow> bool" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
29 |
"wt_method G C pTs rT mxl ins phi \<equiv> |
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> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
33 |
(\<forall>pc. pc<max_pc \<longrightarrow> wt_instr (ins ! pc) G rT phi max_pc pc)" |
8011 | 34 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
35 |
wt_jvm_prog :: "[jvm_prog,prog_type] \<Rightarrow> bool" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
36 |
"wt_jvm_prog G phi \<equiv> |
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: |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
43 |
"wt_jvm_prog G phi \<Longrightarrow> (\<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: |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
47 |
"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins); pc < length ins \<rbrakk> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
48 |
\<Longrightarrow> 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: |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
53 |
"\<lbrakk> wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxl,ins) \<rbrakk> \<Longrightarrow> |
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 |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9559
diff
changeset
|
60 |
"succs i pc = [pc+1] \<Longrightarrow> wt_instr i G rT phi max_pc pc = |
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 |