author | nipkow |
Thu, 02 Dec 1999 09:09:30 +0100 | |
changeset 8047 | 3a0c996cf2b2 |
parent 8045 | 816f566c414f |
child 8119 | 60b606eddec8 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/BV/Correct.thy |
2 |
ID: $Id$ |
|
3 |
Author: Cornelia Pusch |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
The invariant for the type safety proof. |
|
7 |
*) |
|
8 |
||
9 |
Correct = BVSpec + |
|
10 |
||
11 |
constdefs |
|
12 |
approx_val :: "[jvm_prog,aheap,val,ty option] \\<Rightarrow> bool" |
|
13 |
"approx_val G h v any \\<equiv> case any of None \\<Rightarrow> True | Some T \\<Rightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T" |
|
14 |
||
15 |
approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \\<Rightarrow> bool" |
|
16 |
"approx_loc G hp loc LT \\<equiv> |
|
17 |
length loc=length LT \\<and> (\\<forall>(val,any)\\<in>set (zip loc LT). approx_val G hp val any)" |
|
18 |
||
19 |
approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \\<Rightarrow> bool" |
|
20 |
"approx_stk G hp stk ST \\<equiv> approx_loc G hp stk (map Some ST)" |
|
21 |
||
22 |
correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \\<Rightarrow> frame \\<Rightarrow> bool" |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
23 |
"correct_frame G hp \\<equiv> \\<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc). |
8011 | 24 |
approx_stk G hp stk ST \\<and> approx_loc G hp loc LT \\<and> |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
25 |
pc < length ins \\<and> length loc=length(snd sig)+maxl+1" |
8011 | 26 |
|
27 |
consts |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
28 |
correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] \\<Rightarrow> bool" |
8011 | 29 |
primrec |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
30 |
"correct_frames G hp phi rT0 sig0 [] = True" |
8011 | 31 |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
32 |
"correct_frames G hp phi rT0 sig0 (f#frs) = |
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
33 |
(let (stk,loc,C,sig,pc) = f; |
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
34 |
(ST,LT) = (phi C sig) ! pc |
8011 | 35 |
in |
36 |
(\\<exists>rT maxl ins. |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
37 |
method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and> |
8032 | 38 |
(\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invoke mn pTs) \\<and> |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
39 |
(mn,pTs) = sig0 \\<and> |
8011 | 40 |
(\\<exists>apTs D ST'. |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
41 |
fst((phi C sig)!k) = (rev apTs) @ (Class D) # ST' \\<and> |
8011 | 42 |
length apTs = length pTs \\<and> |
43 |
(\\<exists>D' rT' maxl' ins'. |
|
8047 | 44 |
method (G,D) sig0 = Some(D',rT',(maxl',ins')) \\<and> |
8011 | 45 |
G \\<turnstile> rT0 \\<preceq> rT') \\<and> |
46 |
correct_frame G hp (tl ST, LT) maxl ins f \\<and> |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
47 |
correct_frames G hp phi rT sig frs))))" |
8011 | 48 |
|
49 |
||
50 |
constdefs |
|
51 |
correct_state :: "[jvm_prog,prog_type,jvm_state] \\<Rightarrow> bool" |
|
8032 | 52 |
("_,_\\<turnstile>JVM _\\<surd>" [51,51] 50) |
8011 | 53 |
"correct_state G phi \\<equiv> \\<lambda>(xp,hp,frs). |
54 |
case xp of |
|
55 |
None \\<Rightarrow> (case frs of |
|
56 |
[] \\<Rightarrow> True |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
57 |
| (f#fs) \\<Rightarrow> G\\<turnstile>h hp\\<surd> \\<and> |
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
58 |
(let (stk,loc,C,sig,pc) = f |
8011 | 59 |
in |
60 |
\\<exists>rT maxl ins. |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
61 |
method (G,C) sig = Some(C,rT,(maxl,ins)) \\<and> |
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
62 |
correct_frame G hp ((phi C sig) ! pc) maxl ins f \\<and> |
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
63 |
correct_frames G hp phi rT sig fs)) |
8011 | 64 |
| Some x \\<Rightarrow> True" |
65 |
||
66 |
end |