Changeset 2615

Timestamp:

Feb 6, 2013, 3:51:53 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

• Papers/itp-2013/ccexec.tex (modified) (1 diff)

Papers/itp-2013/ccexec.tex

@@ -870 +870 @@
 one state, missing one of the two emissions.
 
+\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{trace\_any\_any\_free}~s_a~s_2')$ such that:
+$s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of
+the two call states are the same, $s_1 \mathcal{C} s_b$, the predicate
+$(\texttt{as\_execute}~s_b~s_a)$ holds, $s_1' \mathcal{L} s_b$ and
+$s_1' \mathcal{S} s_2'$.
+\end{condition}
+
+The condition says that, to simulate a function call, we can perform a
+sequence of silent actions before and after the function call itself.
+The old and new call states must be $\mathcal{C}$-related, the old and new
+states at the beginning of the function execution must be $\mathcal{L}$-related
+and, finally, the two initial and final states must be $\mathcal{S}$-related
+as usual.
+
 \begin{verbatim}
 definition status_simulation ≝
-  λS1 : abstract_status.
-  λS2 : abstract_status.
-  λsim_status_rel : status_rel S1 S2.
-    ∀st1,st1',st2.as_execute S1 st1 st1' →
-    sim_status_rel st1 st2 →
-    match as_classify … st1 with
-    [ None ⇒ True
-    | Some cl ⇒
-      match cl with
-      [ cl_call ⇒ ∀prf.
-        (* 
-             st1' ------------S----------\
-              ↑ \                         \
-             st1 \--L--\                   \
-              | \       \                   \
-              S  \-C-\  st2_after_call →taa→ st2'
-              |       \     ↑
-             st2 →taa→ st2_pre_call
-        *)
-        ∃st2_pre_call.
-        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
-        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
-        ∃st2_after_call,st2'.
-        ∃taa2 : trace_any_any … st2 st2_pre_call.
-        ∃taa2' : trace_any_any … st2_after_call st2'.
-        as_execute … st2_pre_call st2_after_call ∧
-        sim_status_rel st1' st2' ∧
-        label_rel … st1' st2_after_call
       | cl_return ⇒
         (*