Ignore:
Timestamp:
Feb 6, 2013, 10:28:57 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec.tex

    r2630 r2631  
    10001000\end{comment}
    10011001
     1002\begin{alltt}
     1003record status_rel (S1,S2 : abstract_status) : Type[1] := \{
     1004  \(\mathcal{S}\): S1 \(\to\) S2 \(\to\) Prop;
     1005  \(\mathcal{C}\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\) (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop
     1006  \}.
     1007
     1008definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.
     1009
     1010definition \(\mathcal{R}\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
     1011 \(\forall\)s1_pre,s2_pre.
     1012  as_after_return s1_pre s1_ret \(\to\) call_rel s1_pre s2_pre \(\to\)
     1013   as_after_return s2_pre s2_ret.
     1014\end{alltt}
     1015
    10021016\begin{theorem}[\texttt{status\_simulation\_produce\_tlr}]
    10031017For every $s_1,s_1',s_{2_b},s_2$ s.t.
Note: See TracChangeset for help on using the changeset viewer.