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