# Changeset 557 for Deliverables/D4.1/ITP-Paper/itp-2011.tex

Ignore:
Timestamp:
Feb 17, 2011, 2:52:34 PM (9 years ago)
Message:

Emulator fixed for Wilmer

File:
1 edited

### Legend:

Unmodified
 r556 In Section~\ref{sect.conclusions} we conclude the paper. In Appendices~\ref{sect.listing.main.ocaml.functions} and~\ref{sect.listing.main.matita.functions} we provide a brief overview of the main functions in our implementation, and describe at a high level what they do. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % SECTION                                                                      % Matita's syntax is largely straightforward to those familiar with Coq or O'Caml. The only subtlety is the use of \texttt{?}' in an argument position denoting an argument that should be inferred automatically. A full account of the formalisation can be found in~\cite{cerco-report:2011}. \subsection{Development strategy} The formalization of MCS-51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits). To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans. In our O'Caml emulator, we faked' bitvectors using phantom types implemented with polymorphic variants\cite{phantom_types_ocaml}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}. In our O'Caml emulator, we `faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}. From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes. However, the module's interface (right column) enforces the size invariants in the rest of the code. \bibliography{itp-2011.bib} \end{document} \newpage