Changeset 1455


Ignore:
Timestamp:
Oct 23, 2011, 5:51:04 PM (8 years ago)
Author:
mulligan
Message:

ratios changed

File:
1 edited

Legend:

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

    r1454 r1455  
    328328  call_dest_for_main: call_dest p;
    329329
    330   succ_pc: succ p $\rightarrow$ address $\rightarrow$ res address;
    331 
    332330  greg_store_: generic_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT;
    333331  greg_retrieve_: regsT $\rightarrow$ generic_reg p $\rightarrow$ res beval;
     
    339337  ...
    340338  pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT;
    341   pointer_of_label: label $\rightarrow$ $\Sigma$p:pointer. ptype p = Code
    342339}.
    343340\end{lstlisting}
    344341Here, the fields \texttt{empty\_framesT}, \texttt{empty\_regsT}, \texttt{call\_args\_for\_main} and \texttt{call\_dest\_for\_main} are used for state initialisation.
    345 
    346 The field \texttt{succ\_pc} takes an address, and a `successor' label, and returns the address of the instruction immediately succeeding the one at hand.
    347342
    348343The fields \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively.
     
    358353We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}:
    359354\begin{lstlisting}
    360 record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] :=
     355record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] :=
    361356{
    362357  more_sparams1 :> more_sem_params p;
     358
     359  succ_pc: succ p $\rightarrow$ address $\rightarrow$ res address;
     360  pointer_of_label: label $\rightarrow$ $\Sigma$p:pointer. ptype p = Code;
     361  ...
    363362  fetch_statement:
    364363    genv ... p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$
     
    382381 }.
    383382\end{lstlisting}
     383The field \texttt{succ\_pc} takes an address, and a `successor' label, and returns the address of the instruction immediately succeeding the one at hand.
     384
    384385Here, \texttt{fetch\_statement} fetches the next statement to be executed.
    385386The fields \texttt{save\_frame} and \texttt{pop\_frame} manipulate stack frames.
     
    613614Description & Matita & Lines & O'Caml & Lines & Ratio \\
    614615\hline
    615 Semantics of the abstracted languages & \texttt{joint/semantics.ma} & 64 & N/A & N/A & N/A  \\
    616 Generic utilities used in semantics `joint' languages & \texttt{joint/SemanticUtils.ma} & 77 & N/A & N/A & N/A \\
     616Semantics of the abstracted languages & \texttt{joint/semantics.ma} & 434 & N/A & N/A & N/A  \\
     617Generic utilities used in semantics `joint' languages & \texttt{joint/SemanticUtils.ma} & 70 & N/A & N/A & N/A \\
    617618Semantics of RTLabs & \texttt{RTLabs/semantics.ma} & 223 & \texttt{RTLabs/RTLabsInterpret.ml} & 355 & 0.63 \\
    618 Semantics of RTL & \texttt{RTL/semantics.ma} & 121 & \texttt{RTL/RTLInterpret.ml} & 324 & 1.88\tnote{a} \\
    619 Semantics of ERTL & \texttt{ERTL/semantics.ma} & 125 & \texttt{ERTL/ERTLInterpret.ml} & 504  & 1.22\tnote{a} \\
    620 Semantics of the joint LTL-LIN language & \texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & 64 & N/A & N/A & N/A \\
    621 Semantics of LTL & \texttt{LTL/semantics.ma} & 6 & \texttt{LTL/LTLInterpret.ml} & 416 & 1.25\tnote{b} \\
    622 Semantics of LIN & \texttt{LIN/semantics.ma} & 22 & \texttt{LIN/LINInterpret.ml} & 379 & 1.52\tnote{b}
     619Semantics of RTL & \texttt{RTL/semantics.ma} & 173 & \texttt{RTL/RTLInterpret.ml} & 324 & 2.01\tnote{a} \\
     620Semantics of ERTL & \texttt{ERTL/semantics.ma} & 130 & \texttt{ERTL/ERTLInterpret.ml} & 504  & 1.26\tnote{a} \\
     621Semantics of the joint LTL-LIN language & \texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & 67 & N/A & N/A & N/A \\
     622Semantics of LTL & \texttt{LTL/semantics.ma} & 5 & \texttt{LTL/LTLInterpret.ml} & 416 & 1.38\tnote{b} \\
     623Semantics of LIN & \texttt{LIN/semantics.ma} & 43 & \texttt{LIN/LINInterpret.ml} & 379 & 1.62\tnote{b}
    623624\end{tabular}
    624625\begin{tablenotes}
     
    626627  \item{b} Includes \texttt{joint/semantics.ma}, \texttt{joint/SemanticUtils.ma} and \texttt{joint/joint\_LTL\_LIN\_semantics.ma}. \\
    627628 \begin{tabular}{ll}
    628   Total lines of Matita code for the above files:& 1125 \\
     629  Total lines of Matita code for the above files:& 1145 \\
    629630  Total lines of O'Caml code for the above files:& 1978 \\
    630   Ration of total lines:& 0.57
     631  Ration of total lines:& 0.58
    631632 \end{tabular}
    632633\end{tablenotes}
Note: See TracChangeset for help on using the changeset viewer.