Changeset 2614 for Papers/itp-2013


Ignore:
Timestamp:
Feb 6, 2013, 3:39:17 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r2613 r2614  
    851851put the labelling approach in motion.
    852852
    853 \begin{condition}[Case \texttt{cl\_other}]
    854  For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
    855  $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
     853\begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}]
     854 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and
     855 $\texttt{as\_execute}~s_1~s_1'$, and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ or $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ and
     856$(\texttt{as\_costed}~s_1')$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
    856857$taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}.
    857858\end{condition}
    858859
    859 The intuition is that one step can be replaced with zero or more steps if it
     860In the above condition, a $(\texttt{trace\_any\_any\_free}~s_1~s_2)$ is an
     861inductive type of structured traces that do not contain function calls or
     862cost emission statements. Differently from a \texttt{trace\_any\_any}, the
     863instruction to be executed in the lookahead state $s_2$ may be a cost emission
     864statement.
     865
     866The intuition of the condition is that one step can be replaced with zero or more steps if it
    860867preserves the relation between the data and if the two final statuses are
    861868labelled in the same way. Moreover, we must take special care of the empty case
     
    915922        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
    916923        ret_rel … sim_status_rel st1' st2_after_ret ∧
    917         label_rel … st1' st2'
    918       | cl_other ⇒
    919           (*         
    920           st1 → st1'
    921             |      \
    922             S      S,L
    923             |        \
    924            st2 →taaf→ st2'
    925            
    926            the taaf can be empty (e.g. tunneling) but we ask it must not be the
    927            case when both st1 and st1' are labelled (we would be able to collapse
    928            labels otherwise)
    929          *)
    930         ∃st2'.
    931         ∃taa2 : trace_any_any_free … st2 st2'.
    932         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    933         sim_status_rel st1' st2' ∧
    934         label_rel … st1' st2'
    935       | cl_jump ⇒
    936         (* just like cl_other, but with a hypothesis more *)
    937         as_costed … st1' →
    938         ∃st2'.
    939         ∃taa2 : trace_any_any_free … st2 st2'.
    940         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    941         sim_status_rel st1' st2' ∧
    942924        label_rel … st1' st2'
    943925      ]
Note: See TracChangeset for help on using the changeset viewer.