Changeset 538


Ignore:
Timestamp:
Feb 16, 2011, 4:51:59 PM (6 years ago)
Author:
mulligan
Message:

Fixed overview of paper, and finished describing continuations.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r537 r538  
    212212\label{subsect.overview.paper}
    213213
    214 In Section~\ref{sect.development.strategy} we provide a brief overview of how we designed and implemented the formalised microprocessor emulator.
    215 In Section~\ref{sect.design.issues.formalisation} we describe how we made use of dependent types to handle some of the idiosyncracies of the microprocessor.
    216 In Section~\ref{sect.related.work} we describe the relation our work has to
     214In Section~\ref{sect.design.issues.formalisation} we discuss design issues in the development of the formalisation.
     215In Section~\ref{sect.validation} we discuss how we validated the design and implementation of our emulator to ensure that what we formalised was an accurate model of an MCS-51 series microprocessor.
     216In Section~\ref{sect.related.work} we describe previous work, with an eye toward describing its relation with the work described herein.
     217In Section~\ref{sect.conclusions} we conclude the paper.
    217218
    218219%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    227228\label{subsect.development.strategy}
    228229
    229 Our implementation progressed in two stages:
    230 
    231 \paragraph{O'Caml prototype}
     230Our implementation progressed in two stages.
    232231We began with an emulator written in O'Caml.
    233232We used this to `iron out' any bugs in our design and implementation within O'Caml's more permissive type system.
     
    235234Once we were happy with the performance and design of the O'Caml emulator, we moved to the Matita formalisation.
    236235
    237 \paragraph{Matita formalisation}
    238236Matita's syntax is lexically similar to O'Caml's.
    239237This eased the translation, as large swathes of code were merely copy-pasted with minor modifications.
Note: See TracChangeset for help on using the changeset viewer.