Changeset 1440 for Deliverables/D4.2-4.3

Timestamp:

Oct 21, 2011, 5:50:06 PM (8 years ago)

Author:

mulligan

Message:

ratios fixed

File:

• Deliverables/D4.2-4.3/reports/D4-2.tex (modified) (2 diffs)

Deliverables/D4.2-4.3/reports/D4-2.tex

@@ -428 +428 @@
 
 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,
-and to provide certified verifiers in Matita. At the moment, the implementation
-of the certified verifiers is left as future work.
+and to provide certified verifiers in Matita.
+At the moment, the implementation of the certified verifiers is left as future work.
 \item
 \textbf{A few non-computational proof obligations.}
@@ -561 +561 @@
 \texttt{joint/TranslateUtils.ma} & Generic translation utilities & N/A & N/A \\
 \texttt{RTLabs/RTLabsToRTL.ma} & Translation from RTLabs to RTL & \texttt{RTLabs/RTLabsToRTL.ml} & 1.61 \\
-\texttt{RTL/RTLToERTL.ma} & Translation from RTL to ERTL & \texttt{RTL/RTLToERTL.ml} & 1.38\tnote{a} \\
-\texttt{RTL/RTLTailcall.ma} & Elimination of tailcalls & \texttt{RTL/RTLtailcall.ml} & 2.01 \\
-\texttt{ERTL/ERTLToLTL.ma} & Translation from ERTL to LTL & \texttt{ERTL/ERTLToLTL.ml} & 1.39\tnote{b} \\
-\texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.23\tnote{c} \\
-\texttt{ERTL/liveness.ma} & Liveness analysis & \texttt{ERTL/liveness.ml} & 1.46\tnote{c} \\
-\texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 1.10\tnote{d} \\
+\texttt{RTL/RTLToERTL.ma} & Translation from RTL to ERTL & \texttt{RTL/RTLToERTL.ml} & 1.01\tnote{a} \\
+\texttt{RTL/RTLTailcall.ma} & Elimination of tailcalls & \texttt{RTL/RTLtailcall.ml} & 2.02 \\
+\texttt{ERTL/ERTLToLTL.ma} & Translation from ERTL to LTL & \texttt{ERTL/ERTLToLTL.ml} & 1.22\tnote{b} \\
+\texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.03\tnote{c} \\
+\texttt{ERTL/liveness.ma} & Liveness analysis & \texttt{ERTL/liveness.ml} & 0.92 \\
+\texttt{LTL/LTLToLIN.ma} & Translation from LTL to LIN & \texttt{LTL/LTLToLIN.ml} & 0.53 \tnote{c} \\
 \texttt{LIN/joint\_LTL\_LIN.ma} & Generic code for LTL and LIN languages & N/A & N/A \\
-\texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 4.06\tnote{e}
+\texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 2.85\tnote{d}
 \end{tabular}
 \begin{tablenotes}
-  \item[a] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma} and \texttt{joint/TranslateUtil.ma}.
-  \item[b] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and\\ \texttt{ERTL/ERTLToLTLI.ml}.
-  \item[c] Includes \texttt{joint/Joint.ma}.
-  \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}.
-  \item[e] Includes \texttt{joint/TranslateUtils.ma}, \texttt{joint/Joint.ma}, \texttt{joint/TranslateUtil.ma} and\\ \texttt{joint/joint\_LTL\_LIN.ma}.\\
-  \begin{tabular}{ll}
-  Total lines of Matita code for the above files:& 3032. \\
-  Total lines of O'Caml code for the above files:& 3332. \\
-  Ration of total lines:& 0.91.
-  \end{tabular}
+  \item[a] Includes \texttt{joint/TranslateUtils.ma}.
+  \item[b] Includes \texttt{joint/TranslateUtils.ma} and \texttt{ERTL/ERTLToLTLI.ml}.
+  \item[c] Includes \texttt{joint/TranslateUtils.ma}, \texttt{LTL/LTLToLINI.ml} and \texttt{joint/joint\_LTL\_LIN.ma}.
+  \item[d] Includes \texttt{joint/TranslateUtils.ma}, and \texttt{joint/joint\_LTL\_LIN.ma}.\\
+  Total lines of Matita code for the above files: 3032. \\
+  Total lines of O'Caml code for the above files: 3332. \\
+  Ration of total lines: 0.91.
 \end{tablenotes}
 \end{threeparttable}