Changeset 2626 for Papers/itp2013/ccexec.tex
 Timestamp:
 Feb 6, 2013, 9:32:13 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2625 r2626 895 895 896 896 \begin{condition}[Case \texttt{cl\_return}] 897 For all $s_1,s_1',s_2$ s uch that $s_1 \mathcal{S} s_1'$ and898 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_return}$, there exists $s_2', s_b, s_a$, a $taa$ of type899 $ (\texttt{trace\_any\_any}~s_2~s_b)$, a $taaf$ of type900 $ (\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:897 For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$, 898 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_return}$, there exists $s_2', s_b, s_a$, a 899 $\texttt{trace\_any\_any}~s_2~s_b$, a 900 $\texttt{trace\_any\_any\_free}~s_a~s_2'$ called $taaf$ such that: 901 901 $s_a$ is classified as a \texttt{cl\_return}, 902 902 $s_1 \mathcal{C} s_b$, the predicate 903 $ (\texttt{as\_execute}~s_b~s_a)$ holds,903 $\texttt{as\_execute}~s_b~s_a$ holds, 904 904 $s_1' \mathcal{R} s_a$ and 905 905 $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either … … 1065 1065 of a traditional, function properties only, proof. 1066 1066 1067 All theresults presented in the paper are part of a larger certification of a1067 All results presented in the paper are part of a larger certification of a 1068 1068 C compiler which is based on the labelling approach. The certification, done 1069 in Matita, is the main deliverable of the European Project CerCo.1069 in Matita, is the main deliverable of the FETOpen Certified Complexity (CerCo). 1070 1070 1071 1071 The short term future work consists in the completion of the certification of … … 1089 1089 function constitutes then a cost model for the source code, in the spirit of 1090 1090 what we are doing in CerCo. However, we believe our solution to be superior 1091 in the following points: 1) the machinery of the labelling approach is1091 in the following respects: 1) the machinery of the labelling approach is 1092 1092 insensible to the resource being measured. Indeed, any cost model computed on 1093 1093 the object code can be lifted to the source code (e.g. stack space used, … … 1100 1100 models can be induced when the approach is scaled to cover, for instance, 1101 1101 loop optimizations~\cite{loopoptimizations}, but the costs are still meant to 1102 be easy to understandable and manipulate in an interactive theorem prover. 1102 be easy to understand and manipulate in an interactive theorem prover or 1103 in FramaC. 1103 1104 On the contrary, a clock function is a complex function of the state $s_1$ 1104 1105 which, as a function, is an opaque object that is difficult to reify as
Note: See TracChangeset
for help on using the changeset viewer.