Changeset 1455 for Deliverables/D4.2-4.3/reports/D4-3.tex
- Timestamp:
- Oct 23, 2011, 5:51:04 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-3.tex
r1454 r1455 328 328 call_dest_for_main: call_dest p; 329 329 330 succ_pc: succ p $\rightarrow$ address $\rightarrow$ res address;331 332 330 greg_store_: generic_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT; 333 331 greg_retrieve_: regsT $\rightarrow$ generic_reg p $\rightarrow$ res beval; … … 339 337 ... 340 338 pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT; 341 pointer_of_label: label $\rightarrow$ $\Sigma$p:pointer. ptype p = Code342 339 }. 343 340 \end{lstlisting} 344 341 Here, 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.347 342 348 343 The fields \texttt{greg\_store\_} and \texttt{greg\_retrieve\_} store and retrieve values from a generic register, respectively. … … 358 353 We extend \texttt{more\_sem\_params} with yet more parameters via \texttt{more\_sem\_params2}: 359 354 \begin{lstlisting} 360 record more_sem_params 2(globals: list ident) (p: params globals) : Type[1] :=355 record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] := 361 356 { 362 357 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 ... 363 362 fetch_statement: 364 363 genv ... p $\rightarrow$ state (mk_sem_params ... more_sparams1) $\rightarrow$ … … 382 381 }. 383 382 \end{lstlisting} 383 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. 384 384 385 Here, \texttt{fetch\_statement} fetches the next statement to be executed. 385 386 The fields \texttt{save\_frame} and \texttt{pop\_frame} manipulate stack frames. … … 613 614 Description & Matita & Lines & O'Caml & Lines & Ratio \\ 614 615 \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} & 7 7& N/A & N/A & N/A \\616 Semantics of the abstracted languages & \texttt{joint/semantics.ma} & 434 & N/A & N/A & N/A \\ 617 Generic utilities used in semantics `joint' languages & \texttt{joint/SemanticUtils.ma} & 70 & N/A & N/A & N/A \\ 617 618 Semantics of RTLabs & \texttt{RTLabs/semantics.ma} & 223 & \texttt{RTLabs/RTLabsInterpret.ml} & 355 & 0.63 \\ 618 Semantics of RTL & \texttt{RTL/semantics.ma} & 1 21 & \texttt{RTL/RTLInterpret.ml} & 324 & 1.88\tnote{a} \\619 Semantics of ERTL & \texttt{ERTL/semantics.ma} & 1 25 & \texttt{ERTL/ERTLInterpret.ml} & 504 & 1.22\tnote{a} \\620 Semantics of the joint LTL-LIN language & \texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & 6 4& 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}619 Semantics of RTL & \texttt{RTL/semantics.ma} & 173 & \texttt{RTL/RTLInterpret.ml} & 324 & 2.01\tnote{a} \\ 620 Semantics of ERTL & \texttt{ERTL/semantics.ma} & 130 & \texttt{ERTL/ERTLInterpret.ml} & 504 & 1.26\tnote{a} \\ 621 Semantics of the joint LTL-LIN language & \texttt{LIN/joint\_LTL\_LIN\_semantics.ma} & 67 & N/A & N/A & N/A \\ 622 Semantics of LTL & \texttt{LTL/semantics.ma} & 5 & \texttt{LTL/LTLInterpret.ml} & 416 & 1.38\tnote{b} \\ 623 Semantics of LIN & \texttt{LIN/semantics.ma} & 43 & \texttt{LIN/LINInterpret.ml} & 379 & 1.62\tnote{b} 623 624 \end{tabular} 624 625 \begin{tablenotes} … … 626 627 \item{b} Includes \texttt{joint/semantics.ma}, \texttt{joint/SemanticUtils.ma} and \texttt{joint/joint\_LTL\_LIN\_semantics.ma}. \\ 627 628 \begin{tabular}{ll} 628 Total lines of Matita code for the above files:& 11 25 \\629 Total lines of Matita code for the above files:& 1145 \\ 629 630 Total lines of O'Caml code for the above files:& 1978 \\ 630 Ration of total lines:& 0.5 7631 Ration of total lines:& 0.58 631 632 \end{tabular} 632 633 \end{tablenotes}
Note: See TracChangeset
for help on using the changeset viewer.