Changeset 2365


Ignore:
Timestamp:
Sep 27, 2012, 5:48:10 PM (7 years ago)
Author:
mulligan
Message:

More minor tweaks.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2364 r2365  
    659659Not 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.
    660660It would not be natural to see the proof that fetch and assembly commute as the specification of one of the two functions.
    661 \paragraph{Related work}
     661
     662\subsection{Related work}
     663\label{subsect.related.work}
    662664% piton
    663665We are not the first to consider the correctness of an assembler for a non-trivial assembly language.
     
    670672Care 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 MCS-51's I/O facilities.
    671673This is only possible by inducing a cost model on the source code from the optimisation strategy and input program.
    672 \paragraph{Resources}
     674
     675\subsection{Resources}
     676\label{subsect.resources}
    673677Our source files are available at~\url{http://cerco.cs.unibo.it}.
    674678We assumed several properties of `library functions', e.g. modular arithmetic and datastructure manipulation.
Note: See TracChangeset for help on using the changeset viewer.