Changeset 1442


Ignore:
Timestamp:
Oct 21, 2011, 6:00:03 PM (9 years ago)
Author:
mulligan
Message:

changes fixing wrong deletion of conflicts

File:
1 edited

Legend:

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

    r1441 r1442  
    427427These axiomatised components are found in the ERTL to LTL pass.
    428428
    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.
    430 Therefore, we plan to provide implementations in OCaml only, and to provide certified verifiers in Matita.
     429It 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,
     430and to provide certified verifiers in Matita.
    431431At the moment, the implementation of the certified verifiers is left as future work.
    432432\item
     
    566566\texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.03\tnote{c} \\
    567567\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} \\
     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 \\
    570570\texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 2.85\tnote{d}
     
    575575  \item[c] Includes \texttt{joint/TranslateUtils.ma}, \texttt{LTL/LTLToLINI.ml} and \texttt{joint/joint\_LTL\_LIN.ma}.
    576576  \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.
     577  \begin{tabular}{ll}
     578  Total lines of Matita code for the above files:& 3032. \\
     579  Total lines of O'Caml code for the above files:& 3332. \\
     580  Ration of total lines:& 0.91.
     581  \end{tabular}
    580582\end{tablenotes}
    581583\end{threeparttable}
Note: See TracChangeset for help on using the changeset viewer.