# Changeset 2626 for Papers/itp-2013/ccexec.tex

Ignore:
Timestamp:
Feb 6, 2013, 9:32:13 PM (7 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2625 \begin{condition}[Case \texttt{cl\_return}] 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\_return}$, there exists $s_2', s_b, s_a$, a $taa$ of type $(\texttt{trace\_any\_any}~s_2~s_b)$, a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that: For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$, $\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 $\texttt{trace\_any\_any}~s_2~s_b$, a $\texttt{trace\_any\_any\_free}~s_a~s_2'$ called $taaf$ such that: $s_a$ is classified as a \texttt{cl\_return}, $s_1 \mathcal{C} s_b$, the predicate $(\texttt{as\_execute}~s_b~s_a)$ holds, $\texttt{as\_execute}~s_b~s_a$ holds, $s_1' \mathcal{R} s_a$ and $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either of a traditional, function properties only, proof. All the results presented in the paper are part of a larger certification of a All results presented in the paper are part of a larger certification of a C compiler which is based on the labelling approach. The certification, done in Matita, is the main deliverable of the European Project CerCo. in Matita, is the main deliverable of the FET-Open Certified Complexity (CerCo). The short term future work consists in the completion of the certification of function constitutes then a cost model for the source code, in the spirit of what we are doing in CerCo. However, we believe our solution to be superior in the following points: 1) the machinery of the labelling approach is in the following respects: 1) the machinery of the labelling approach is insensible to the resource being measured. Indeed, any cost model computed on the object code can be lifted to the source code (e.g. stack space used, models can be induced when the approach is scaled to cover, for instance, loop optimizations~\cite{loopoptimizations}, but the costs are still meant to be easy to understandable and manipulate in an interactive theorem prover. be easy to understand and manipulate in an interactive theorem prover or in Frama-C. On the contrary, a clock function is a complex function of the state $s_1$ which, as a function, is an opaque object that is difficult to reify as