Changeset 1442 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 21, 2011, 6:00:03 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-2.tex
r1441 r1442 427 427 These axiomatised components are found in the ERTL to LTL pass. 428 428 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.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. 431 431 At the moment, the implementation of the certified verifiers is left as future work. 432 432 \item … … 566 566 \texttt{ERTL/Interference.ma} & Axiomatised graph colouring component & \texttt{common/interference.ml} & 0.03\tnote{c} \\ 567 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 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 570 \texttt{LIN/LINToASM.ma} & Translation from LIN to assembly & \texttt{LIN/LINToASM.ml} & 2.85\tnote{d} … … 575 575 \item[c] Includes \texttt{joint/TranslateUtils.ma}, \texttt{LTL/LTLToLINI.ml} and \texttt{joint/joint\_LTL\_LIN.ma}. 576 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. 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} 580 582 \end{tablenotes} 581 583 \end{threeparttable}
Note: See TracChangeset
for help on using the changeset viewer.