Index: /Papers/cppasm2012/cpp2012asm.tex
===================================================================
 /Papers/cppasm2012/cpp2012asm.tex (revision 2363)
+++ /Papers/cppasm2012/cpp2012asm.tex (revision 2364)
@@ 138,5 +138,10 @@
The rest of this paper is a detailed description of our proof that is marginally still a work in progress.
\paragraph{Matita}
+
+%  %
+% SECTION %
+%  %
+\section{Matita}
+\label{sect.matita}
Matita is a proof assistant based on a variant of the Calculus of (Co)inductive Constructions~\cite{asperti:user:2007}.
It features dependent types that we exploit in the formalisation.
@@ 324,5 +329,5 @@
Conceptually the assembler works in two passes.
The first pass expands every pseudoinstruction into a list of machine code instructions using the function \texttt{expand\_pseudo\_instruction}. The policy
determines which expansion among the alternatives will be choosed for
+determines which expansion among the alternatives will be chosen for
pseudojumps and pseudocalls. Once the expansion is performed, the cost
of the pseudoinstruction is defined as the cost of the expansion.
@@ 376,9 +381,9 @@
still to be performed when expanding the instruction at \texttt{ppc}.
To solve the issue, we define the policy \texttt{policy} as a maps
from a valid pseudoaddress to the corresponding address in the assembled
+To solve the issue, we define the policy \texttt{policy} as a map
+from a valid pseudoaddress to the corresponding address in the assembled
program.
Therefore, $\delta$ in the example above can be computed simply as
\texttt{sigma(a)  sigma(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that
+\texttt{policy(a)  policy(ppc + 1)}. Moreover, the \texttt{expand\_pseudo\_instruction} emits a \texttt{SJMP} only after verifying for each \texttt{Jmp} that
$\delta < 128$. When this is not the case, the function emits an
\texttt{AJMP} if possible, or an \texttt{LJMP} otherwise, therefore always
@@ 394,5 +399,5 @@
the sum of the size of all the expansions of the pseudoinstructions that
preceed the one at address \texttt{a}: the assembler just concatenates all
expansions one after another. To grant this property, we impose a
+expansions sequentially. To grant this property, we impose a
correctness criterion over policies. A policy is correct when for all
valid pseudoaddresses \texttt{ppc}
@@ 654,6 +659,5 @@
Not every proof has been carried out in this way: we only used this style to prove that a function satisfies a specification that only involves that function in a significant way.
It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions.
%\paragraph{Related work}

+\paragraph{Related work}
% piton
We are not the first to consider the correctness of an assembler for a nontrivial assembly language.
@@ 666,6 +670,5 @@
Care must be taken to ensure that the time properties of an assembly program are not modified by assembly lest we affect the semantics of any program employing the MCS51's I/O facilities.
This is only possible by inducing a cost model on the source code from the optimisation strategy and input program.
%\paragraph{Resources}

+\paragraph{Resources}
Our source files are available at~\url{http://cerco.cs.unibo.it}.
We assumed several properties of `library functions', e.g. modular arithmetic and datastructure manipulation.