Changeset 506


Ignore:
Timestamp:
Feb 14, 2011, 11:55:13 AM (6 years ago)
Author:
mulligan
Message:

a bit more added

File:
1 edited

Legend:

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

    r505 r506  
    172172\label{sect.from.o'caml.prototype.matita.formalisation}
    173173
    174 Our implementation followed a two-layered approach.
     174Our implementation progressed in two stages:
    175175
    176176\paragraph{O'Caml prototype}
    177 Our implementation began with an emulator written in O'Caml.
    178 This served the purpose of allowing us to `iron out' any bugs in the design of the emulator within a more permissive language.
    179 Further,
     177We began with an emulator written in O'Caml.
     178We used this to `iron out' any bugs in our design and implementation within O'Caml's more permissive type system.
     179O'Caml's ability to perform file input-output also eased debugging and validation.
     180Once we were happy with the performance and design of the O'Caml emulator, we moved to the Matita formalisation.
    180181
    181182\paragraph{Matita formalisation}
     183Matita's syntax is lexically similar to O'Caml's.
     184This eased the translation, as large swathes of code were merely copy-pasted with minor modifications.
     185However, several major issues had to be addresses when moving from O'Caml to Matita.
     186These are now discussed.
    182187
    183188%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    186191\section{Design issues in the formalisation}
    187192\label{sect.design.issues.formalisation}
     193
     194As mentioned, the emulator formalisation is part of a wider project, CerCo.
     195In parallel with the implementation of the emulator was the construction of a prototype compiler targetting the MCS-51.
    188196
    189197%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.