Changeset 1440 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 21, 2011, 5:50:06 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-2.tex
r1439 r1440 428 428 429 429 It should be noted that these axiomatised components fall into the following pattern: whilst their implementation is complex, and their proof of correctness is difficult, we are able to quickly and easily verify that any answer that they provide is correct. Therefore, we plan to provide implementations in OCaml only, 430 and to provide certified verifiers in Matita. At the moment, the implementation431 of the certified verifiers is left as future work.430 and to provide certified verifiers in Matita. 431 At the moment, the implementation of the certified verifiers is left as future work. 432 432 \item 433 433 \textbf{A few non-computational proof obligations.} … … 561 561 \texttt{joint/TranslateUtils.ma} & Generic translation utilities & N/A & N/A \\ 562 562 \texttt{RTLabs/RTLabsToRTL.ma} & Translation from RTLabs to RTL & \texttt{RTLabs/RTLabsToRTL.ml} & 1.61 \\ 563 \texttt{RTL/RTLToERTL.ma} & Translation from RTL to ERTL & \texttt{RTL/RTLToERTL.ml} & 1. 38\tnote{a} \\564 \texttt{RTL/RTLTailcall.ma} & Elimination of tailcalls & \texttt{RTL/RTLtailcall.ml} & 2.0 1\\565 \texttt{ERTL/ERTLToLTL.ma} & Translation from ERTL to LTL & \texttt{ERTL/ERTLToLTL.ml} & 1. 39\tnote{b} \\566 \texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0. 23\tnote{c} \\567 \texttt{ERTL/liveness.ma} & Liveness analysis & \texttt{ERTL/liveness.ml} & 1.46\tnote{c}\\568 \texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 1.10\tnote{d} \\563 \texttt{RTL/RTLToERTL.ma} & Translation from RTL to ERTL & \texttt{RTL/RTLToERTL.ml} & 1.01\tnote{a} \\ 564 \texttt{RTL/RTLTailcall.ma} & Elimination of tailcalls & \texttt{RTL/RTLtailcall.ml} & 2.02 \\ 565 \texttt{ERTL/ERTLToLTL.ma} & Translation from ERTL to LTL & \texttt{ERTL/ERTLToLTL.ml} & 1.22\tnote{b} \\ 566 \texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.03\tnote{c} \\ 567 \texttt{ERTL/liveness.ma} & Liveness analysis & \texttt{ERTL/liveness.ml} & 0.92 \\ 568 \texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 0.53 \tnote{c} \\ 569 569 \texttt{LIN/joint\_LTL\_LIN.ma} & Generic code for LTL and LIN languages & N/A & N/A \\ 570 \texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 4.06\tnote{e}570 \texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 2.85\tnote{d} 571 571 \end{tabular} 572 572 \begin{tablenotes} 573 \item[a] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma} and \texttt{joint/TranslateUtil.ma}. 574 \item[b] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and\\ \texttt{ERTL/ERTLToLTLI.ml}. 575 \item[c] Includes \texttt{joint/Joint.ma}. 576 \item[d] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma}, \texttt{LTL/LTLToLINI.ml} and \texttt{joint/joint\_LTL\_LIN.ma}. 577 \item[e] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and\\ \texttt{joint/joint\_LTL\_LIN.ma}.\\ 578 \begin{tabular}{ll} 579 Total lines of Matita code for the above files:& 3032. \\ 580 Total lines of O'Caml code for the above files:& 3332. \\ 581 Ration of total lines:& 0.91. 582 \end{tabular} 573 \item[a] Includes \texttt{joint/TranslateUtils.ma}. 574 \item[b] Includes \texttt{joint/TranslateUtils.ma} and \texttt{ERTL/ERTLToLTLI.ml}. 575 \item[c] Includes \texttt{joint/TranslateUtils.ma}, \texttt{LTL/LTLToLINI.ml} and \texttt{joint/joint\_LTL\_LIN.ma}. 576 \item[d] Includes \texttt{joint/TranslateUtils.ma}, and \texttt{joint/joint\_LTL\_LIN.ma}.\\ 577 Total lines of Matita code for the above files: 3032. \\ 578 Total lines of O'Caml code for the above files: 3332. \\ 579 Ration of total lines: 0.91. 583 580 \end{tablenotes} 584 581 \end{threeparttable}
Note: See TracChangeset
for help on using the changeset viewer.