Changeset 3306 for Papers/itp2013/ccexec.tex
 Timestamp:
 May 30, 2013, 5:28:20 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r3305 r3306 89 89 every node/.style={draw, is other}}, 90 90 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, 91 95 } 92 96 … … 106 110 107 111 \newcommand{\append}{\mathbin{@}} 112 \newcommand{\iffdef}{\mathrel{:\Leftrightarrow}} 108 113 109 114 \begin{document} … … 392 397 The program semantics adopted in the traditional labelling approach is based 393 398 on labelled deductive systems. Given a set of observables $\mathcal{O}$ and 394 a set of states $\ mathcal{S}$, the semantics of one deterministic execution399 a set of states $\S$, the semantics of one deterministic execution 395 400 step is 396 401 defined as a function $S \to S \times O^*$ where $O^*$ is a (finite) stream of … … 727 732 kind  are defined by structural recursion on the first trace and pattern 728 733 matching 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 734 the definition into the inference rules shown in \autoref{fig:txx_rel} 735 for the sake of readability. We also omit from trace constructors all arguments, 736 but those that are traces or that 731 737 are used in the premises of the rules. By abuse of notation we denote all three 732 relations by infixing $\approx$ 733 738 relations by infixing $\approx$. 739 740 \begin{figure} 734 741 \begin{multicols}{2} 735 742 \infrule … … 744 751 {\texttt{tlr\_step}~tll_1~tlr_1 \approx \texttt{tlr\_step}~tll_2~tlr_2} 745 752 \end{multicols} 746 753 \vspace{3ex} 754 \begin{multicols}{2} 747 755 \infrule 748 756 {\ell~s_1 = \ell~s_2 \andalso … … 752 760 753 761 \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 754 768 {} 755 769 {\texttt{tal\_base\_not\_return}\approx taa \append \texttt{tal\_base\_not\_return}} 756 770 \vspace{1ex} 757 771 \infrule 758 772 {} 759 773 {\texttt{tal\_base\_return}\approx taa \append \texttt{tal\_base\_return}} 760 774 \vspace{1ex} 761 775 \infrule 762 776 {tlr_1\approx tlr_2 \andalso … … 764 778 } 765 779 {\texttt{tal\_base\_call}~s_1~tlr_1\approx taa \append \texttt{tal\_base\_call}~s_2~tlr_2} 766 780 \vspace{1ex} 767 781 \infrule 768 782 {tlr_1\approx tlr_2 \andalso … … 771 785 } 772 786 {\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} 774 788 \infrule 775 789 {tlr_1\approx tlr_2 \andalso … … 778 792 } 779 793 {\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} 781 795 \infrule 782 796 {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 784 798 tal_1 \approx tal_2 \andalso 785 799 } 786 800 {\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 % 792 805 \begin{comment} 793 806 \begin{verbatim} … … 863 876 \end{verbatim} 864 877 \end{comment} 865 878 % 866 879 In the preceding rules, a $taa$ is an inhabitant of the 867 880 $\texttt{trace\_any\_any}~s_1~s_2$ (shorthand $\texttt{TAA}~s_1~s_2$), … … 873 886 left of a \texttt{TAL}. A \texttt{TAA} captures 874 887 a sequence of silent moves. 875 876 888 The \texttt{tal\_collapsable} unary predicate over \texttt{TAL}'s 877 889 holds when the argument does not contain any function call and it ends … … 879 891 can still perform a sequence of silent actions while remaining similar. 880 892 893 As should be expected, even though the rules are asymmetric $\approx$ is in fact 894 an equivalence relation. 881 895 \section{Forward simulation} 882 896 \label{simulation} … … 894 908 simulation we are interested in (preservation of observables), we are 895 909 forced to prove a stronger notion of forward simulation that introduces 896 an explicit relation between states. The classical notion of a 1to 0ormany897 forward simulation is the existence of a relation $ R$ over states such that898 if $s_1 Rs_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that899 $s_2 \to^* s_2'$ and $s_1' Rs_2'$. In our context, we need to replace the910 an explicit relation between states. The classical notion of a 1tomany 911 forward simulation is the existence of a relation $\S$ over states such that 912 if $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 900 914 one and multi step transition relations $\to^n$ with the existence of 901 915 a structured trace between the two states, and we need to add the request that … … 903 917 something like:\\ 904 918 for all $s_1,s_2,s_1'$ such that there is a $\tau_1$ from 905 $s_1$ to $s_1'$ and $s_1 Rs_2$ there exists an $s_2'$ such that906 $s_1' Rs_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that919 $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 907 921 $\tau_1$ is similar to $\tau_2$. We call this particular form of forward 908 922 simulation \emph{trace reconstruction}. … … 937 951 938 952 Therefore we now introduce an abstract notion of relation set between abstract 939 statuses and an abstract notion of 1to 0ormany forward simulation conditions.953 statuses and an abstract notion of 1tomany forward simulation conditions. 940 954 These two definitions enjoy the following remarkable properties: 941 955 \begin{enumerate} 942 956 \item they are generic enough to accommodate all passes of the CerCo compiler 943 \item the conjunction of the 1to 0ormany forward simulation conditions are944 just slightly stricter than the statement of a 1to 0ormany forward957 \item the conjunction of the 1tomany forward simulation conditions are 958 just slightly stricter than the statement of a 1tomany forward 945 959 simulation in the classical case. In particular, they only require 946 960 the construction of very simple forms of structured traces made of 947 961 silent states only. 948 \item they allow to prove our main result of the paper: the 1to 0ormany962 \item they allow to prove our main result of the paper: the 1tomany 949 963 forward simulation conditions are sufficient to prove the trace 950 964 reconstruction theorem … … 960 974 that the cost model can be computed on the object code and lifted to the 961 975 source code to reason on nonfunctional properties, assuming that 962 the 1to 0ormany forward simulation conditions are fulfilled for every976 the 1tomany forward simulation conditions are fulfilled for every 963 977 compiler pass. 964 978 … … 970 984 by every pass. The remaining two are derived relations. 971 985 972 The $\ mathcal{S}$ relation between states is the classical relation used986 The $\S$ relation between states is the classical relation used 973 987 in forward simulation proofs. It correlates the data of the status 974 988 (e.g. registers, memory, etc.). 975 989 976 The $\ mathcal{C}$ relation correlates call states. It allows to track the990 The $\C$ relation correlates call states. It allows to track the 977 991 position in the target code of every call in the source code. 978 992 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 993 The $\L$ relation simply says that the two states are both label 994 emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$. 995 It allows to track the position in 981 996 the target code of every cost emitting statement in the source code. 982 997 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'$. 998 Finally 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 1000 successors 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.$$ 987 1003 We will require all pairs of states that follow a related call to be 988 $\ mathcal{R}$related. This is the fundamental requirement to grant989 that the target trace is well structured, i.e. that functioncalls are well990 nested and always returnwhere 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 1005 that the target trace is well structured, \emph{i.e.}\ that calls are well 1006 nested 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} 1005 1021 1006 1022 \begin{figure} 1007 1023 \centering 1008 \begin{tabular}{@{}c@{}c@{} }1009 \begin{subfigure}{.475\linewidth}1010 \centering1011 \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} 1030 1046 \centering 1031 1047 \begin{tikzpicture}[every join/.style={ar}, join all, thick, … … 1042 1058 \draw [new] (t1) to node [rel] {$\S,\L$} (t2); 1043 1059 \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} 1046 1062 \end{subfigure} 1047 \\ 1048 \begin{subfigure}{. 475\linewidth}1063 & 1064 \begin{subfigure}{.375\linewidth} 1049 1065 \centering 1050 1066 \begin{tikzpicture}[every join/.style={ar}, join all, thick, … … 1071 1087 \end{subfigure} 1072 1088 & 1073 \begin{subfigure}{. 475\linewidth}1089 \begin{subfigure}{.375\linewidth} 1074 1090 \centering 1075 1091 \begin{tikzpicture}[every join/.style={ar}, join all, thick, … … 1095 1111 \end{subfigure} 1096 1112 \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. 1098 1114 Dashed lines 1099 1115 and arrows indicates how the diagrams must be closed when solid relations … … 1102 1118 \end{figure} 1103 1119 1104 \paragraph{1to 0ormany forward simulation conditions.}1120 \paragraph{1tomany forward simulation conditions.} 1105 1121 \begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}] 1106 1122 For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and … … 1112 1128 \end{condition} 1113 1129 1114 In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ (which from now on 1130 In the above condition depicted in \autoref{subfig:cl_other_jump}, 1131 a $\texttt{trace\_any\_any\_free}~s_1~s_2$ (which from now on 1115 1132 will be shorthanded as \verb+TAAF+) is an 1116 1133 inductive type of structured traces that do not contain function calls or … … 1130 1147 $\verb+TAAF+~s_b~s_2'$ such that: 1131 1148 $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$,1149 the two call states are the same, $s_1 \C s_a$, 1133 1150 $s_a\exec s_b$, $s_1' \L s_b$ and 1134 1151 $s_1' \S s_2'$. 1135 1152 \end{condition} 1136 1153 1137 The condition says that, to simulate a function call, we can perform a1154 The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a 1138 1155 sequence 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 new1140 states at the beginning of the function execution must be $\ mathcal{L}$related1141 and, finally, the two initial and final states must be $\ mathcal{S}$related1156 The old and new call states must be $\C$related, the old and new 1157 states at the beginning of the function execution must be $\L$related 1158 and, finally, the two initial and final states must be $\S$related 1142 1159 as usual. 1143 1160 … … 1147 1164 $\verb+TAA+~s_2~s_a$, a 1148 1165 $\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}$, 1150 1167 $s_a\exec s_b$, 1151 1168 $s_1' \R s_b$ and … … 1155 1172 1156 1173 Similarly 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, 1174 sequence of silent actions before and after the return statement itself, 1175 as depicted in \autoref{subfig:cl_return}. 1176 The old and the new statements after the return must be $\R$related, 1159 1177 to grant that they returned to corresponding calls. 1160 The two initial and final states must be $\ mathcal{S}$related1178 The two initial and final states must be $\S$related 1161 1179 as usual and, moreover, they must exhibit the same labels. Finally, when 1162 1180 the suffix is non empty we must take care of not inserting a new … … 1247 1265 \end{comment} 1248 1266 1249 \paragraph{Main result: the 1to 0ormany forward simulation conditions1267 \paragraph{Main result: the 1tomany forward simulation conditions 1250 1268 are sufficient to trace reconstruction} 1251 1269 1252 Let us assume that a relation set is given such that the 1to 0ormany1270 Let us assume that a relation set is given such that the 1tomany 1253 1271 forward simulation conditions are satisfied. Under this assumption we 1254 1272 can prove the following three trace reconstruction theorems by mutual … … 1283 1301 precomputed preamble, even if this is likely to be the case in concrete 1284 1302 implementations. The preamble in input is necessary for compositionality, e.g. 1285 because the 1to 0ormany forward simulation conditions allow in the1303 because the 1tomany forward simulation conditions allow in the 1286 1304 case of function calls to execute a preamble of silent instructions just after 1287 1305 the function call. 1288 1306 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. 1307 Clearly similar results are also available for the other two types of structured 1308 traces (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. 1338 1358 1339 1359 \begin{comment} … … 1341 1361 For every $s_1,s_1',s_2$ s.t. 1342 1362 there 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$ 1344 1364 there exists $s_{2_m},s_2'$ s.t. 1345 1365 there is a $\texttt{trace\_label\_return}~s_2~s_{2_m}$ called $tlr_2$ and … … 1347 1367 s.t. if $taaf$ is non empty then $\lnot (\texttt{as\_costed}~s_{2_m})$, 1348 1368 and $\texttt{tlr\_rel}~tlr_1~tlr_2$ 1349 and $s_1' (\ mathcal{S} \cap \mathcal{L}) s_2'$ and1350 $s_1' \ mathcal{R}s_{2_m}$.1369 and $s_1' (\S \cap \L) s_2'$ and 1370 $s_1' \R s_{2_m}$. 1351 1371 \end{corollary} 1352 1372 \end{comment} … … 1415 1435 simulation related to nonfunctional properties (preservation of structure) 1416 1436 from that related to functional properties. In particular, we reduce the 1417 problem of preservation of structure to that of showing a 1to 0ormany1437 problem of preservation of structure to that of showing a 1tomany 1418 1438 forward simulation that only adds a few additional proof obligations to those 1419 1439 of a traditional, function properties only, proof.
Note: See TracChangeset
for help on using the changeset viewer.