Changeset 1446


Ignore:
Timestamp:
Oct 21, 2011, 6:21:59 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r1434 r1446  
    214214  ...
    215215  | OP1: Op1 $\rightarrow$ acc_a_reg p $\rightarrow$ acc_a_reg p $\rightarrow$ joint_instruction p globals
     216  | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals
    216217  ...
    217218\end{lstlisting}
     
    237238\end{lstlisting}
    238239Note that in the joint language, instructions are `linear', in that they have an immediate successor.
    239 Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program.
     240Statements, on the other hand, consist of either a linear instruction, or a \texttt{GOTO} or \texttt{RETURN} statement, both of which can jump to an arbitrary place in the program. The conditional jump instruction COND is `linear', since it
     241has an immediate successor, but it also takes an arbitrary location (a label)
     242to jump to.
    240243
    241244For the semantics, we need further parametererised types.
     
    557560Should this decision be taken, this will likely be straightforward but potentially time consuming.
    558561
    559 \newpage
    560 
    561562%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
    562563% SECTION.                                                                    %
     
    573574Semantics specific files (files relating to language translations ommitted).
    574575Syntax specific files are presented in Table~\ref{table.syntax}.
     576Here, the O'Caml column denotes the O'Caml source file(s) in the prototype compiler's implementation that corresponds to the Matita script in question.
     577The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file.
     578These are computed with \texttt{wc -l}, a standard Unix tool.
     579
     580Individual file's ratios are an over approximation, due to the fact that it's hard to relate an individual O'Caml file to the abstracted Matita code that has been spread across multiple files.
     581The ratio between total Matita code lines and total O'Caml code lines is more reflective of the compressed and abstracted state of the Matita translation.
     582
     583Semantics specific files are presented in Table~\ref{table.semantics}.
    575584\begin{landscape}
    576585\begin{table}
     
    599608\end{table}
    600609\end{landscape}
    601 Here, the O'Caml column denotes the O'Caml source file(s) in the prototype compiler's implementation that corresponds to the Matita script in question.
    602 The ratios are the linecounts of the Matita file divided by the line counts of the corresponding O'Caml file.
    603 These are computed with \texttt{wc -l}, a standard Unix tool.
    604 
    605 Individual file's ratios are an over approximation, due to the fact that it's hard to relate an individual O'Caml file to the abstracted Matita code that has been spread across multiple files.
    606 The ratio between total Matita code lines and total O'Caml code lines is more reflective of the compressed and abstracted state of the Matita translation.
    607 
    608 Semantics specific files are presented in Table~\ref{table.semantics}.
    609610\begin{landscape}
    610611\begin{table}
     
    618619\texttt{RTL/semantics.ma} & Semantics of RTL & \texttt{RTL/RTLInterpret.ml} & 1.88\tnote{a} \\
    619620\texttt{ERTL/semantics.ma} & Semantics of ERTL & \texttt{ERTL/ERTLInterpret.ml} & 1.22\tnote{a} \\
     621\texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & Semantics of the joint LTL-LIN language & N/A & N/A \\
    620622\texttt{LTL/semantics.ma} & Semantics of LTL & \texttt{LTL/LTLInterpret.ml} & 1.25\tnote{c} \\
    621 \texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & Semantics of the joint LTL-LIN language & N/A & N/A \\
    622623\texttt{LIN/semantics.ma} & Semantics of LIN & \texttt{LIN/LINInterpret.ml} & 1.52\tnote{c}
    623624\end{tabular}
     
    626627  \item{b} Includes \texttt{joint/joint\_LTL\_LIN\_semantics.ma}.
    627628  \item{c} Includes \texttt{joint/semantics.ma}, \texttt{joint/SemanticUtils.ma} and \texttt{joint/joint\_LTL\_LIN\_semantics.ma}. \\
    628   Total lines of Matita code for the above files: 1125. \\
    629   Total lines of O'Caml code for the above files: 1978. \\
    630   Ration of total lines: 0.57.
     629 \begin{tabular}{ll}
     630  Total lines of Matita code for the above files:& 1125 \\
     631  Total lines of O'Caml code for the above files:& 1978 \\
     632  Ration of total lines:& 0.57
     633 \end{tabular}
    631634\end{tablenotes}
    632635\end{threeparttable}
Note: See TracChangeset for help on using the changeset viewer.