Changeset 2614 for Papers/itp2013
 Timestamp:
 Feb 6, 2013, 3:39:17 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2613 r2614 851 851 put the labelling approach in motion. 852 852 853 \begin{condition}[Case \texttt{cl\_other}] 854 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and 855 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either 853 \begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}] 854 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and 855 $\texttt{as\_execute}~s_1~s_1'$, and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ or $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ and 856 $(\texttt{as\_costed}~s_1')$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either 856 857 $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}. 857 858 \end{condition} 858 859 859 The intuition is that one step can be replaced with zero or more steps if it 860 In the above condition, a $(\texttt{trace\_any\_any\_free}~s_1~s_2)$ is an 861 inductive type of structured traces that do not contain function calls or 862 cost emission statements. Differently from a \texttt{trace\_any\_any}, the 863 instruction to be executed in the lookahead state $s_2$ may be a cost emission 864 statement. 865 866 The intuition of the condition is that one step can be replaced with zero or more steps if it 860 867 preserves the relation between the data and if the two final statuses are 861 868 labelled in the same way. Moreover, we must take special care of the empty case … … 915 922 as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ 916 923 ret_rel … sim_status_rel st1' st2_after_ret ∧ 917 label_rel … st1' st2'918  cl_other ⇒919 (*920 st1 → st1'921  \922 S S,L923  \924 st2 →taaf→ st2'925 926 the taaf can be empty (e.g. tunneling) but we ask it must not be the927 case when both st1 and st1' are labelled (we would be able to collapse928 labels otherwise)929 *)930 ∃st2'.931 ∃taa2 : trace_any_any_free … st2 st2'.932 (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧933 sim_status_rel st1' st2' ∧934 label_rel … st1' st2'935  cl_jump ⇒936 (* just like cl_other, but with a hypothesis more *)937 as_costed … st1' →938 ∃st2'.939 ∃taa2 : trace_any_any_free … st2 st2'.940 (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧941 sim_status_rel st1' st2' ∧942 924 label_rel … st1' st2' 943 925 ]
Note: See TracChangeset
for help on using the changeset viewer.