Changeset 2616 for Papers


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

...

File:
1 edited

Legend:

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

    r2615 r2616  
    872872\begin{condition}[Case \texttt{cl\_call}]
    873873 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 $taaf_1$ of type
    875 $(\texttt{trace\_any\_any\_free}~s_2~s_b)$, a $taaf_2$ of type
     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_1$ of type
     875$(\texttt{trace\_any\_any}~s_2~s_b)$, a $taa_2$ of type
    876876$(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
    877877$s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of
     
    888888as usual.
    889889
    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
     903Similarly to the call condition, to simulate a return we can perform a
     904sequence of silent actions before and after the return statement itself.
     905The old and the new statements after the return must be $\mathcal{R}$-related,
     906to grant that they returned to corresponding calls.
     907The two initial and final states must be $\mathcal{S}$-related
     908as usual and, moreover, they must exhibit the same labels. Finally, when
     909the suffix is non empty we must take care of not inserting a new
     910unmatched cost emission statement just after the return statement.
     911
    918912\begin{comment}
    919913\begin{verbatim}
Note: See TracChangeset for help on using the changeset viewer.