 Timestamp:
 Feb 6, 2013, 10:28:57 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2630 r2631 1000 1000 \end{comment} 1001 1001 1002 \begin{alltt} 1003 record 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 1008 definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2. 1009 1010 definition \(\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 1002 1016 \begin{theorem}[\texttt{status\_simulation\_produce\_tlr}] 1003 1017 For every $s_1,s_1',s_{2_b},s_2$ s.t.
Note: See TracChangeset
for help on using the changeset viewer.