Changeset 1440


Ignore:
Timestamp:
Oct 21, 2011, 5:50:06 PM (8 years ago)
Author:
mulligan
Message:

ratios fixed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.2-4.3/reports/D4-2.tex

    r1439 r1440  
    428428
    429429It 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 implementation
    431 of the certified verifiers is left as future work.
     430and to provide certified verifiers in Matita.
     431At the moment, the implementation of the certified verifiers is left as future work.
    432432\item
    433433\textbf{A few non-computational proof obligations.}
     
    561561\texttt{joint/TranslateUtils.ma} & Generic translation utilities & N/A & N/A \\
    562562\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.01 \\
    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} \\
    569569\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}
    571571\end{tabular}
    572572\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.
    583580\end{tablenotes}
    584581\end{threeparttable}
Note: See TracChangeset for help on using the changeset viewer.