Changeset 2615 for Papers


Ignore:
Timestamp:
Feb 6, 2013, 3:51:53 PM (6 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r2614 r2615  
    870870one state, missing one of the two emissions.
    871871
     872\begin{condition}[Case \texttt{cl\_call}]
     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 $taaf_1$ of type
     875$(\texttt{trace\_any\_any\_free}~s_2~s_b)$, a $taaf_2$ of type
     876$(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
     877$s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of
     878the two call states are the same, $s_1 \mathcal{C} s_b$, the predicate
     879$(\texttt{as\_execute}~s_b~s_a)$ holds, $s_1' \mathcal{L} s_b$ and
     880$s_1' \mathcal{S} s_2'$.
     881\end{condition}
     882
     883The condition says that, to simulate a function call, we can perform a
     884sequence of silent actions before and after the function call itself.
     885The old and new call states must be $\mathcal{C}$-related, the old and new
     886states at the beginning of the function execution must be $\mathcal{L}$-related
     887and, finally, the two initial and final states must be $\mathcal{S}$-related
     888as usual.
     889
    872890\begin{verbatim}
    873891definition status_simulation ≝
    874   λS1 : abstract_status.
    875   λS2 : abstract_status.
    876   λsim_status_rel : status_rel S1 S2.
    877     ∀st1,st1',st2.as_execute S1 st1 st1' →
    878     sim_status_rel st1 st2 →
    879     match as_classify … st1 with
    880     [ None ⇒ True
    881     | Some cl ⇒
    882       match cl with
    883       [ cl_call ⇒ ∀prf.
    884         (*
    885              st1' ------------S----------\
    886               ↑ \                         \
    887              st1 \--L--\                   \
    888               | \       \                   \
    889               S  \-C-\  st2_after_call →taa→ st2'
    890               |       \     ↑
    891              st2 →taa→ st2_pre_call
    892         *)
    893         ∃st2_pre_call.
    894         as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
    895         call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
    896         ∃st2_after_call,st2'.
    897         ∃taa2 : trace_any_any … st2 st2_pre_call.
    898         ∃taa2' : trace_any_any … st2_after_call st2'.
    899         as_execute … st2_pre_call st2_after_call ∧
    900         sim_status_rel st1' st2' ∧
    901         label_rel … st1' st2_after_call
    902892      | cl_return ⇒
    903893        (*
Note: See TracChangeset for help on using the changeset viewer.