37 "correct_frames G hp phi rT0 sig0 [] = True" |
37 "correct_frames G hp phi rT0 sig0 [] = True" |
38 |
38 |
39 "correct_frames G hp phi rT0 sig0 (f#frs) = |
39 "correct_frames G hp phi rT0 sig0 (f#frs) = |
40 (let (stk,loc,C,sig,pc) = f in |
40 (let (stk,loc,C,sig,pc) = f in |
41 (\<exists>ST LT rT maxs maxl ins. |
41 (\<exists>ST LT rT maxs maxl ins. |
42 phi C sig ! pc = Some (ST,LT) \<and> |
42 phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and> |
43 method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and> |
43 method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and> |
44 (\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and> |
44 (\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and> |
45 (mn,pTs) = sig0 \<and> |
45 (mn,pTs) = sig0 \<and> |
46 (\<exists>apTs D ST' LT'. |
46 (\<exists>apTs D ST' LT'. |
47 (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \<and> |
47 (phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \<and> |
48 length apTs = length pTs \<and> |
48 length apTs = length pTs \<and> |
49 (\<exists>D' rT' maxs' maxl' ins'. |
49 (\<exists>D' rT' maxs' maxl' ins'. |
62 [] => True |
62 [] => True |
63 | (f#fs) => G\<turnstile>h hp\<surd> \<and> |
63 | (f#fs) => G\<turnstile>h hp\<surd> \<and> |
64 (let (stk,loc,C,sig,pc) = f |
64 (let (stk,loc,C,sig,pc) = f |
65 in |
65 in |
66 \<exists>rT maxs maxl ins s. |
66 \<exists>rT maxs maxl ins s. |
|
67 is_class G C \<and> |
67 method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and> |
68 method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and> |
68 phi C sig ! pc = Some s \<and> |
69 phi C sig ! pc = Some s \<and> |
69 correct_frame G hp s maxl ins f \<and> |
70 correct_frame G hp s maxl ins f \<and> |
70 correct_frames G hp phi rT sig fs)) |
71 correct_frames G hp phi rT sig fs)) |
71 | Some x => True" |
72 | Some x => True" |