# Changeset 2616 for Papers/itp-2013

Ignore:
Timestamp:
Feb 6, 2013, 4:07:13 PM (8 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2615 \begin{condition}[Case \texttt{cl\_call}] For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and $\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 $taaf_1$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_b)$, a $taaf_2$ of type $\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 $(\texttt{trace\_any\_any}~s_2~s_b)$, a $taa_2$ of type $(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that: $s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of as usual. \begin{verbatim} definition status_simulation ≝ | cl_return ⇒ (* st1 / ↓ | st1'----------S,L------------\ S   \                           \ \   \-----R-------\            | \                 |           | st2 →taa→ st2_ret |           | ↓   /            | st2_after_ret →taaf→ st2' we also ask that st2_after_ret be not labelled if the taaf tail is not empty *) ∃st2_ret,st2_after_ret,st2'. ∃taa2 : trace_any_any … st2 st2_ret. ∃taa2' : trace_any_any_free … st2_after_ret st2'. (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ as_classifier … st2_ret cl_return ∧ as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ ret_rel … sim_status_rel st1' st2_after_ret ∧ label_rel … st1' st2' ] ]. \end{verbatim} \begin{condition}[Case \texttt{cl\_return}] For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and $\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 $(\texttt{trace\_any\_any}~s_2~s_b)$, a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that: $s_a$ is classified as a \texttt{cl\_return}, $s_1 \mathcal{C} s_b$, the predicate $(\texttt{as\_execute}~s_b~s_a)$ holds, $s_1' \mathcal{R} s_a$ and $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either $taaf$ is non empty, or $s_a$ is not \texttt{as\_costed}. \end{condition} Similarly to the call condition, to simulate a return we can perform a sequence of silent actions before and after the return statement itself. The old and the new statements after the return must be $\mathcal{R}$-related, to grant that they returned to corresponding calls. The two initial and final states must be $\mathcal{S}$-related as usual and, moreover, they must exhibit the same labels. Finally, when the suffix is non empty we must take care of not inserting a new unmatched cost emission statement just after the return statement. \begin{comment} \begin{verbatim}