Changeset 2616
 Timestamp:
 Feb 6, 2013, 4:07:13 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2615 r2616 872 872 \begin{condition}[Case \texttt{cl\_call}] 873 873 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and 874 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a $taa f_1$ of type875 $(\texttt{trace\_any\_any \_free}~s_2~s_b)$, a $taaf_2$ of type874 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a $taa_1$ of type 875 $(\texttt{trace\_any\_any}~s_2~s_b)$, a $taa_2$ of type 876 876 $(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that: 877 877 $s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of … … 888 888 as usual. 889 889 890 \begin{verbatim} 891 definition status_simulation ≝ 892  cl_return ⇒ 893 (* 894 st1 895 / ↓ 896  st1'S,L\ 897 S \ \ 898 \ \R\  899 \   900 st2 →taa→ st2_ret   901 ↓ /  902 st2_after_ret →taaf→ st2' 903 904 we also ask that st2_after_ret be not labelled if the taaf tail is 905 not empty 906 *) 907 ∃st2_ret,st2_after_ret,st2'. 908 ∃taa2 : trace_any_any … st2 st2_ret. 909 ∃taa2' : trace_any_any_free … st2_after_ret st2'. 910 (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ 911 as_classifier … st2_ret cl_return ∧ 912 as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ 913 ret_rel … sim_status_rel st1' st2_after_ret ∧ 914 label_rel … st1' st2' 915 ] 916 ]. 917 \end{verbatim} 890 \begin{condition}[Case \texttt{cl\_return}] 891 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and 892 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_return}$, there exists $s_2', s_b, s_a$, a $taa$ of type 893 $(\texttt{trace\_any\_any}~s_2~s_b)$, a $taaf$ of type 894 $(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that: 895 $s_a$ is classified as a \texttt{cl\_return}, 896 $s_1 \mathcal{C} s_b$, the predicate 897 $(\texttt{as\_execute}~s_b~s_a)$ holds, 898 $s_1' \mathcal{R} s_a$ and 899 $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either 900 $taaf$ is non empty, or $s_a$ is not \texttt{as\_costed}. 901 \end{condition} 902 903 Similarly to the call condition, to simulate a return we can perform a 904 sequence of silent actions before and after the return statement itself. 905 The old and the new statements after the return must be $\mathcal{R}$related, 906 to grant that they returned to corresponding calls. 907 The two initial and final states must be $\mathcal{S}$related 908 as usual and, moreover, they must exhibit the same labels. Finally, when 909 the suffix is non empty we must take care of not inserting a new 910 unmatched cost emission statement just after the return statement. 911 918 912 \begin{comment} 919 913 \begin{verbatim}
Note: See TracChangeset
for help on using the changeset viewer.