(* Title: HOL/MicroJava/BV/Correct.thy
ID: $Id$
Author: Cornelia Pusch
Copyright 1999 Technische Universitaet Muenchen
The invariant for the type safety proof.
*)
Correct = BVSpec +
constdefs
approx_val :: "[jvm_prog,aheap,val,ty option] \\<Rightarrow> bool"
"approx_val G h v any \\<equiv> case any of None \\<Rightarrow> True | Some T \\<Rightarrow> G,h\\<turnstile>v\\<Colon>\\<preceq>T"
approx_loc :: "[jvm_prog,aheap,val list,locvars_type] \\<Rightarrow> bool"
"approx_loc G hp loc LT \\<equiv>
length loc=length LT \\<and> (\\<forall>(val,any)\\<in>set (zip loc LT). approx_val G hp val any)"
approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] \\<Rightarrow> bool"
"approx_stk G hp stk ST \\<equiv> approx_loc G hp stk (map Some ST)"
correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] \\<Rightarrow> frame \\<Rightarrow> bool"
"correct_frame G hp \\<equiv> \\<lambda>(ST,LT) maxl ins (stk,loc,C,ml,pc).
approx_stk G hp stk ST \\<and> approx_loc G hp loc LT \\<and>
pc < length ins \\<and> length loc=length(snd ml)+maxl+1"
consts
correct_frames :: "[jvm_prog,aheap,prog_type,ty,cname,sig,frame list] \\<Rightarrow> bool"
primrec
"correct_frames G hp phi rT0 C0 ml0 [] = False"
"correct_frames G hp phi rT0 C0 ml0 (f#frs) =
(let (stk,loc,C,ml,pc) = f;
(ST,LT) = (phi C ml) ! pc
in
(\\<exists>rT maxl ins.
cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
(\\<exists>mn pTs k. pc = k+1 \\<and> ins!k = MI(Invokevirtual mn pTs) \\<and>
(mn,pTs) = ml0 \\<and>
(\\<exists>apTs D ST'.
fst((phi C ml)!k) = (rev apTs) @ (Class D) # ST' \\<and>
length apTs = length pTs \\<and>
(\\<exists>D' rT' maxl' ins'.
cmethd (G,D) (mn,pTs) = Some(D',rT',(maxl',ins')) \\<and>
G \\<turnstile> rT0 \\<preceq> rT') \\<and>
correct_frame G hp (tl ST, LT) maxl ins f \\<and>
correct_frames G hp phi rT C ml frs))))"
constdefs
correct_state :: "[jvm_prog,prog_type,jvm_state] \\<Rightarrow> bool"
"correct_state G phi \\<equiv> \\<lambda>(xp,hp,frs).
case xp of
None \\<Rightarrow> (case frs of
[] \\<Rightarrow> True
| (f#fs) \\<Rightarrow> (let (stk,loc,C,ml,pc) = f
in
\\<exists>rT maxl ins.
cmethd (G,C) ml = Some(C,rT,(maxl,ins)) \\<and>
G,hp\\<turnstile>\\<surd> \\<and>
correct_frame G hp ((phi C ml) ! pc) maxl ins f \\<and>
correct_frames G hp phi rT C ml fs))
| Some x \\<Rightarrow> True"
end