Changeset 3306


Ignore:
Timestamp:
May 30, 2013, 5:28:20 PM (4 years ago)
Author:
tranquil
Message:

altre modifiche e qualche taglio (i risultati per tll e tal)

File:
1 edited

Legend:

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

    r3305 r3306  
    8989                      every node/.style={draw, is other}},
    9090         small vgap/.style={row sep={7mm,between origins}},
     91         % for article, maybe temporary
     92         is jump/.style=is other,
     93         is call/.style=is other,
     94         is ret/.style=is other,
    9195}
    9296
     
    106110
    107111\newcommand{\append}{\mathbin{@}}
     112\newcommand{\iffdef}{\mathrel{:\Leftrightarrow}}
    108113
    109114\begin{document}
     
    392397The program semantics adopted in the traditional labelling approach is based
    393398on labelled deductive systems. Given a set of observables $\mathcal{O}$ and
    394 a set of states $\mathcal{S}$, the semantics of one deterministic execution
     399a set of states $\S$, the semantics of one deterministic execution
    395400step is
    396401defined as a function $S \to S \times O^*$ where $O^*$ is a (finite) stream of
     
    727732kind --- are defined by structural recursion on the first trace and pattern
    728733matching over the second. Here we turn
    729 the definition into inference rules for the sake of readability. We also
    730 omit from trace constructors all arguments, but those that are traces or that
     734the definition into the inference rules shown in \autoref{fig:txx_rel}
     735for the sake of readability. We also omit from trace constructors all arguments,
     736but those that are traces or that
    731737are used in the premises of the rules. By abuse of notation we denote all three
    732 relations by infixing $\approx$
    733 
     738relations by infixing $\approx$.
     739
     740\begin{figure}
    734741\begin{multicols}{2}
    735742\infrule
     
    744751 {\texttt{tlr\_step}~tll_1~tlr_1 \approx \texttt{tlr\_step}~tll_2~tlr_2}
    745752\end{multicols}
    746 
     753\vspace{3ex}
     754\begin{multicols}{2}
    747755\infrule
    748756 {\ell~s_1 = \ell~s_2 \andalso
     
    752760
    753761\infrule
     762 {tal_1\approx tal_2
     763 }
     764 {\texttt{tal\_step\_default}~tal_1 \approx tal_2}
     765\end{multicols}
     766\vspace{3ex}
     767\infrule
    754768 {}
    755769 {\texttt{tal\_base\_not\_return}\approx taa \append \texttt{tal\_base\_not\_return}}
    756 
     770\vspace{1ex}
    757771\infrule
    758772 {}
    759773 {\texttt{tal\_base\_return}\approx taa \append \texttt{tal\_base\_return}}
    760 
     774\vspace{1ex}
    761775\infrule
    762776 {tlr_1\approx tlr_2 \andalso
     
    764778 }
    765779 {\texttt{tal\_base\_call}~s_1~tlr_1\approx taa \append \texttt{tal\_base\_call}~s_2~tlr_2}
    766 
     780\vspace{1ex}
    767781\infrule
    768782 {tlr_1\approx tlr_2 \andalso
     
    771785 }
    772786 {\texttt{tal\_base\_call}~s_1~tlr_1 \approx taa \append \texttt{tal\_step\_call}~s_2~tlr_2~tal_2)}
    773 
     787\vspace{1ex}
    774788\infrule
    775789 {tlr_1\approx tlr_2 \andalso
     
    778792 }
    779793 {\texttt{tal\_step\_call}~s_1~tlr_1~tal_1 \approx taa \append \texttt{tal\_base\_call}~s_2~tlr_2)}
    780 
     794\vspace{1ex}
    781795\infrule
    782796 {tlr_1 \approx tlr_2 \andalso
    783   s_1 \uparrow f \andalso s_2\uparrow f
     797  s_1 \uparrow f \andalso s_2\uparrow f\andalso
    784798  tal_1 \approx tal_2 \andalso
    785799 }
    786800 {\texttt{tal\_step\_call}~s_1~tlr_1~tal_1 \approx taa \append \texttt{tal\_step\_call}~s_2~tlr_2~tal_2}
    787 
    788 \infrule
    789  {tal_1\approx tal_2
    790  }
    791  {\texttt{tal\_step\_default}~tal_1 \approx tal_2}
     801\caption{The inference rule for the relation $\approx$.}
     802\label{fig:txx_rel}
     803\end{figure}
     804%
    792805\begin{comment}
    793806\begin{verbatim}
     
    863876\end{verbatim}
    864877\end{comment}
    865 
     878%
    866879In the preceding rules, a $taa$ is an inhabitant of the
    867880$\texttt{trace\_any\_any}~s_1~s_2$ (shorthand $\texttt{TAA}~s_1~s_2$),
     
    873886left of a \texttt{TAL}. A \texttt{TAA} captures
    874887a sequence of silent moves.
    875 
    876888The \texttt{tal\_collapsable} unary predicate over \texttt{TAL}'s
    877889holds when the argument does not contain any function call and it ends
     
    879891can still perform a sequence of silent actions while remaining similar.
    880892
     893As should be expected, even though the rules are asymmetric $\approx$ is in fact
     894an equivalence relation.
    881895\section{Forward simulation}
    882896\label{simulation}
     
    894908simulation we are interested in (preservation of observables), we are
    895909forced to prove a stronger notion of forward simulation that introduces
    896 an explicit relation between states. The classical notion of a 1-to-0-or-many
    897 forward simulation is the existence of a relation $R$ over states such that
    898 if $s_1 R s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that
    899 $s_2 \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the
     910an explicit relation between states. The classical notion of a 1-to-many
     911forward simulation is the existence of a relation $\S$ over states such that
     912if $s_1 \S s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that
     913$s_2 \to^* s_2'$ and $s_1' \S s_2'$. In our context, we need to replace the
    900914one and multi step transition relations $\to^n$ with the existence of
    901915a structured trace between the two states, and we need to add the request that
     
    903917something like:\\
    904918for all $s_1,s_2,s_1'$ such that there is a $\tau_1$ from
    905 $s_1$ to $s_1'$ and $s_1 R s_2$ there exists an $s_2'$ such that
    906 $s_1' R s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that
     919$s_1$ to $s_1'$ and $s_1 \S s_2$ there exists an $s_2'$ such that
     920$s_1' \S s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that
    907921$\tau_1$ is similar to $\tau_2$. We call this particular form of forward
    908922simulation \emph{trace reconstruction}.
     
    937951
    938952Therefore we now introduce an abstract notion of relation set between abstract
    939 statuses and an abstract notion of 1-to-0-or-many forward simulation conditions.
     953statuses and an abstract notion of 1-to-many forward simulation conditions.
    940954These two definitions enjoy the following remarkable properties:
    941955\begin{enumerate}
    942956 \item they are generic enough to accommodate all passes of the CerCo compiler
    943  \item the conjunction of the 1-to-0-or-many forward simulation conditions are
    944        just slightly stricter than the statement of a 1-to-0-or-many forward
     957 \item the conjunction of the 1-to-many forward simulation conditions are
     958       just slightly stricter than the statement of a 1-to-many forward
    945959       simulation in the classical case. In particular, they only require
    946960       the construction of very simple forms of structured traces made of
    947961       silent states only.
    948  \item they allow to prove our main result of the paper: the 1-to-0-or-many
     962 \item they allow to prove our main result of the paper: the 1-to-many
    949963       forward simulation conditions are sufficient to prove the trace
    950964       reconstruction theorem
     
    960974that the cost model can be computed on the object code and lifted to the
    961975source code to reason on non-functional properties, assuming that
    962 the 1-to-0-or-many forward simulation conditions are fulfilled for every
     976the 1-to-many forward simulation conditions are fulfilled for every
    963977compiler pass.
    964978
     
    970984by every pass. The remaining two are derived relations.
    971985
    972 The $\mathcal{S}$ relation between states is the classical relation used
     986The $\S$ relation between states is the classical relation used
    973987in forward simulation proofs. It correlates the data of the status
    974988(e.g. registers, memory, etc.).
    975989
    976 The $\mathcal{C}$ relation correlates call states. It allows to track the
     990The $\C$ relation correlates call states. It allows to track the
    977991position in the target code of every call in the source code.
    978992
    979 The $\mathcal{L}$ relation simply says that the two states are both label
    980 emitting states that emit the same label. It allows to track the position in
     993The $\L$ relation simply says that the two states are both label
     994emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$.
     995It allows to track the position in
    981996the target code of every cost emitting statement in the source code.
    982997
    983 Finally the $\mathcal{R}$ relation is the more complex one. Two states
    984 $s_1$ and $s_2$ are $\mathcal{R}$ correlated if every time $s_1$ is the
    985 successors of a call state that is $\mathcal{C}$-related to a call state
    986 $s_2'$ in the target code, then $s_2$ is the successor of $s_2'$.
     998Finally the $\R$ relation is the more complex one. Two states
     999$s_1$ and $s_2$ are $\R$ correlated if every time $s_1$ is the
     1000successors of a call state that is $\C$-related to a call state
     1001$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. Formally:
     1002$$s_1\R s_2 \iffdef \forall s_1',s_2'.s_1'\C s_2' \to s_1'\ar s_1 \to s_2' \ar s_2.$$
    9871003We will require all pairs of states that follow a related call to be
    988 $\mathcal{R}$-related. This is the fundamental requirement to grant
    989 that the target trace is well structured, i.e. that function calls are well
    990 nested and always return where they are supposed to.
    991 
    992 \begin{alltt}
    993 record status_rel (S1,S2 : abstract_status) : Type[1] := \{
    994   \(\mathcal{S}\): S1 \(\to\) S2 \(\to\) Prop;
    995   \(\mathcal{C}\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\)
    996      (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop \}.
    997 
    998 definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.
    999 
    1000 definition \(\mathcal{R}\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
    1001  \(\forall\)s1_pre,s2_pre.
    1002   as_after_return s1_pre s1_ret \(\to\) s1_pre \(\mathcal{R}\) s2_pre \(\to\)
    1003    as_after_return s2_pre s2_ret.
    1004 \end{alltt}
     1004$\R$-related. This is the fundamental requirement granting
     1005that the target trace is well structured, \emph{i.e.}\ that calls are well
     1006nested and returning where they are supposed to.
     1007
     1008% \begin{alltt}
     1009% record status_rel (S1,S2 : abstract_status) : Type[1] := \{
     1010%   \(\S\): S1 \(\to\) S2 \(\to\) Prop;
     1011%   \(\C\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\)
     1012%      (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop \}.
     1013%
     1014% definition \(\L\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.
     1015%
     1016% definition \(\R\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
     1017% \(\forall\)s1_pre,s2_pre.
     1018%   as_after_return s1_pre s1_ret \(\to\) s1_pre \(\R\) s2_pre \(\to\)
     1019%    as_after_return s2_pre s2_ret.
     1020% \end{alltt}
    10051021
    10061022\begin{figure}
    10071023\centering
    1008 \begin{tabular}{@{}c@{}c@{}}
    1009 \begin{subfigure}{.475\linewidth}
    1010 \centering
    1011 \begin{tikzpicture}[every join/.style={ar}, join all, thick,
    1012                             every label/.style=overlay, node distance=10mm]
    1013     \matrix [diag] (m) {%
    1014          \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
    1015          \node (s2) {}; & \node (t2) {}; \\
    1016     };
    1017     \node [above=0 of t1, overlay] {$\alpha$};
    1018     {[-stealth]
    1019     \draw (s1) -- (t1);
    1020     \draw [new] (s2) -- node [above] {$*$} (t2);
    1021     }
    1022     \draw (s1) to node [rel] {$\S$} (s2);
    1023     \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
    1024 \end{tikzpicture}
    1025 \caption{The \texttt{cl\_jump} case.}
    1026 \label{subfig:cl_jump}
    1027 \end{subfigure}
    1028 &
    1029 \begin{subfigure}{.475\linewidth}
     1024\begin{tabular}{@{}c@{}c@{}c@{}}
     1025% \begin{subfigure}{.475\linewidth}
     1026% \centering
     1027% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
     1028%                             every label/.style=overlay, node distance=10mm]
     1029%     \matrix [diag] (m) {%
     1030%          \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
     1031%          \node (s2) {}; & \node (t2) {}; \\
     1032%     };
     1033%     \node [above=0 of t1, overlay] {$\alpha$};
     1034%     {[-stealth]
     1035%     \draw (s1) -- (t1);
     1036%     \draw [new] (s2) -- node [above] {$*$} (t2);
     1037%     }
     1038%     \draw (s1) to node [rel] {$\S$} (s2);
     1039%     \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
     1040% \end{tikzpicture}
     1041% \caption{The \texttt{cl\_jump} case.}
     1042% \label{subfig:cl_jump}
     1043% \end{subfigure}
     1044% &
     1045\begin{subfigure}{.25\linewidth}
    10301046\centering
    10311047\begin{tikzpicture}[every join/.style={ar}, join all, thick,
     
    10421058    \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
    10431059\end{tikzpicture}
    1044 \caption{The \texttt{cl\_oher} case.}
    1045 \label{subfig:cl_other}
     1060\caption{The \texttt{cl\_oher} and \texttt{cl\_jump} cases.}
     1061\label{subfig:cl_other_jump}
    10461062\end{subfigure}
    1047 \\
    1048 \begin{subfigure}{.475\linewidth}
     1063&
     1064\begin{subfigure}{.375\linewidth}
    10491065\centering
    10501066\begin{tikzpicture}[every join/.style={ar}, join all, thick,
     
    10711087\end{subfigure}
    10721088&
    1073 \begin{subfigure}{.475\linewidth}
     1089\begin{subfigure}{.375\linewidth}
    10741090\centering
    10751091\begin{tikzpicture}[every join/.style={ar}, join all, thick,
     
    10951111\end{subfigure}
    10961112\end{tabular}
    1097 \caption{The hypotheses for the preservation of structured traces, simplified.
     1113\caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces.
    10981114         Dashed lines
    10991115         and arrows indicates how the diagrams must be closed when solid relations
     
    11021118\end{figure}
    11031119
    1104 \paragraph{1-to-0-or-many forward simulation conditions.}
     1120\paragraph{1-to-many forward simulation conditions.}
    11051121\begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}]
    11061122 For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and
     
    11121128\end{condition}
    11131129
    1114 In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ (which from now on
     1130In the above condition depicted in \autoref{subfig:cl_other_jump},
     1131a $\texttt{trace\_any\_any\_free}~s_1~s_2$ (which from now on
    11151132will be shorthanded as \verb+TAAF+) is an
    11161133inductive type of structured traces that do not contain function calls or
     
    11301147$\verb+TAAF+~s_b~s_2'$ such that:
    11311148$s_a\class\texttt{cl\_call}$, the \texttt{as\_call\_ident}'s of
    1132 the two call states are the same, $s_1 \mathcal{C} s_a$,
     1149the two call states are the same, $s_1 \C s_a$,
    11331150$s_a\exec s_b$, $s_1' \L s_b$ and
    11341151$s_1' \S s_2'$.
    11351152\end{condition}
    11361153
    1137 The condition says that, to simulate a function call, we can perform a
     1154The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a
    11381155sequence of silent actions before and after the function call itself.
    1139 The old and new call states must be $\mathcal{C}$-related, the old and new
    1140 states at the beginning of the function execution must be $\mathcal{L}$-related
    1141 and, finally, the two initial and final states must be $\mathcal{S}$-related
     1156The old and new call states must be $\C$-related, the old and new
     1157states at the beginning of the function execution must be $\L$-related
     1158and, finally, the two initial and final states must be $\S$-related
    11421159as usual.
    11431160
     
    11471164$\verb+TAA+~s_2~s_a$, a
    11481165$\verb+TAAF+~s_b~s_2'$ called $taaf$ such that:
    1149 $s_a$ is classified as a \texttt{cl\_return},
     1166$s_a\class\texttt{cl\_return}$,
    11501167$s_a\exec s_b$,
    11511168$s_1' \R s_b$ and
     
    11551172
    11561173Similarly to the call condition, to simulate a return we can perform a
    1157 sequence of silent actions before and after the return statement itself.
    1158 The old and the new statements after the return must be $\mathcal{R}$-related,
     1174sequence of silent actions before and after the return statement itself,
     1175as depicted in \autoref{subfig:cl_return}.
     1176The old and the new statements after the return must be $\R$-related,
    11591177to grant that they returned to corresponding calls.
    1160 The two initial and final states must be $\mathcal{S}$-related
     1178The two initial and final states must be $\S$-related
    11611179as usual and, moreover, they must exhibit the same labels. Finally, when
    11621180the suffix is non empty we must take care of not inserting a new
     
    12471265\end{comment}
    12481266
    1249 \paragraph{Main result: the 1-to-0-or-many forward simulation conditions
     1267\paragraph{Main result: the 1-to-many forward simulation conditions
    12501268are sufficient to trace reconstruction}
    12511269
    1252 Let us assume that a relation set is given such that the 1-to-0-or-many
     1270Let us assume that a relation set is given such that the 1-to-many
    12531271forward simulation conditions are satisfied. Under this assumption we
    12541272can prove the following three trace reconstruction theorems by mutual
     
    12831301precomputed preamble, even if this is likely to be the case in concrete
    12841302implementations. The preamble in input is necessary for compositionality, e.g.
    1285 because the 1-to-0-or-many forward simulation conditions allow in the
     1303because the 1-to-many forward simulation conditions allow in the
    12861304case of function calls to execute a preamble of silent instructions just after
    12871305the function call.
    12881306
    1289 \begin{theorem}[\texttt{status\_simulation\_produce\_tll}]
    1290 For every $s_1,s_1',s_{2_b},s_2$ s.t.
    1291 there is a $\texttt{TLL}~b~s_1~s_1'$ called $tll_1$ and a
    1292 $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
    1293 $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
    1294 \begin{itemize}
    1295  \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
    1296        and a trace $\texttt{TLL}~b~s_{2_b}~s_{2_m}$ called $tll_2$
    1297        and a $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
    1298        $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
    1299        $s_1' \R s_{2_m}$ and
    1300        $tll_1\approx tll_2$ and
    1301        if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
    1302  \item else there exists $s_2'$ and a
    1303        $\texttt{TLL}~b~s_{2_b}~s_2'$ called $tll_2$ such that
    1304        $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
    1305        $tll_1\approx tll_2$.
    1306 \end{itemize}
    1307 \end{theorem}
    1308 
    1309 The statement is similar to the previous one: a source
    1310 \texttt{trace\_label\_label} and a given target preamble of silent states
    1311 in the target code induce a similar \texttt{trace\_label\_label} in the
    1312 target code, possibly followed by a sequence of silent moves that become the
    1313 preamble for the next \texttt{trace\_label\_label} translation.
    1314 
    1315 \begin{theorem}[\texttt{status\_simulation\_produce\_tal}]
    1316 For every $s_1,s_1',s_2$ s.t.
    1317 there is a $\texttt{TAL}~b~s_1~s_1'$ called $tal_1$ and
    1318 $s_1 \mathcal{S} s_2$
    1319 \begin{itemize}
    1320  \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
    1321    and a trace $\texttt{TAL}~b~s_2~s_{2_m}$ called $tal_2$ and a
    1322    $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
    1323    $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
    1324    $s_1' \R s_{2_m}$ and
    1325    $tal_1 \approx tal_2$ and
    1326    if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
    1327  \item else there exists $s_2'$ and a
    1328    $\texttt{TAL}~b~s_2~s_2'$ called $tal_2$ such that
    1329    either $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
    1330        $tal_1\approx tal_2$
    1331    or $s_1' \mathrel{{\S} \cap {\L}} s_2$ and
    1332    $\texttt{tal\_collapsable}~tal_1$ and $\lnot \ell~s_1$.
    1333 \end{itemize}
    1334 \end{theorem}
    1335 
    1336 The statement is also similar to the previous ones, but for the lack of
    1337 the target code preamble.
     1307Clearly similar results are also available for the other two types of structured
     1308traces (in fact, they are all proved simultaneously by mutual induction).
     1309% \begin{theorem}[\texttt{status\_simulation\_produce\_tll}]
     1310% For every $s_1,s_1',s_{2_b},s_2$ s.t.
     1311% there is a $\texttt{TLL}~b~s_1~s_1'$ called $tll_1$ and a
     1312% $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
     1313% $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
     1314% \begin{itemize}
     1315%  \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
     1316%        and a trace $\texttt{TLL}~b~s_{2_b}~s_{2_m}$ called $tll_2$
     1317%        and a $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
     1318%        $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1319%        $s_1' \R s_{2_m}$ and
     1320%        $tll_1\approx tll_2$ and
     1321%        if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
     1322%  \item else there exists $s_2'$ and a
     1323%        $\texttt{TLL}~b~s_{2_b}~s_2'$ called $tll_2$ such that
     1324%        $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1325%        $tll_1\approx tll_2$.
     1326% \end{itemize}
     1327% \end{theorem}
     1328%
     1329% The statement is similar to the previous one: a source
     1330% \texttt{trace\_label\_label} and a given target preamble of silent states
     1331% in the target code induce a similar \texttt{trace\_label\_label} in the
     1332% target code, possibly followed by a sequence of silent moves that become the
     1333% preamble for the next \texttt{trace\_label\_label} translation.
     1334%
     1335% \begin{theorem}[\texttt{status\_simulation\_produce\_tal}]
     1336% For every $s_1,s_1',s_2$ s.t.
     1337% there is a $\texttt{TAL}~b~s_1~s_1'$ called $tal_1$ and
     1338% $s_1 \S s_2$
     1339% \begin{itemize}
     1340%  \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
     1341%    and a trace $\texttt{TAL}~b~s_2~s_{2_m}$ called $tal_2$ and a
     1342%    $\texttt{TAAF}~s_{2_m}~s_2'$ called $taa_2$ s.t.
     1343%    $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1344%    $s_1' \R s_{2_m}$ and
     1345%    $tal_1 \approx tal_2$ and
     1346%    if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
     1347%  \item else there exists $s_2'$ and a
     1348%    $\texttt{TAL}~b~s_2~s_2'$ called $tal_2$ such that
     1349%    either $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1350%        $tal_1\approx tal_2$
     1351%    or $s_1' \mathrel{{\S} \cap {\L}} s_2$ and
     1352%    $\texttt{tal\_collapsable}~tal_1$ and $\lnot \ell~s_1$.
     1353% \end{itemize}
     1354% \end{theorem}
     1355%
     1356% The statement is also similar to the previous ones, but for the lack of
     1357% the target code preamble.
    13381358
    13391359\begin{comment}
     
    13411361For every $s_1,s_1',s_2$ s.t.
    13421362there is a $\texttt{trace\_label\_return}~s_1~s_1'$ called $tlr_1$ and
    1343 $s_1 (\mathcal{L} \cap \mathcal{S}) s_2$
     1363$s_1 (\L \cap \S) s_2$
    13441364there exists $s_{2_m},s_2'$ s.t.
    13451365there is a $\texttt{trace\_label\_return}~s_2~s_{2_m}$ called $tlr_2$ and
     
    13471367s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$,
    13481368and $\texttt{tlr\_rel}~tlr_1~tlr_2$
    1349 and $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and
    1350 $s_1' \mathcal{R} s_{2_m}$.
     1369and $s_1' (\S \cap \L) s_2'$ and
     1370$s_1' \R s_{2_m}$.
    13511371\end{corollary}
    13521372\end{comment}
     
    14151435simulation related to non-functional properties (preservation of structure)
    14161436from that related to functional properties. In particular, we reduce the
    1417 problem of preservation of structure to that of showing a 1-to-0-or-many
     1437problem of preservation of structure to that of showing a 1-to-many
    14181438forward simulation that only adds a few additional proof obligations to those
    14191439of a traditional, function properties only, proof.
Note: See TracChangeset for help on using the changeset viewer.