Changeset 554


Ignore:
Timestamp:
Feb 17, 2011, 2:09:58 PM (6 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r553 r554  
    231231From hereonin, we typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}} to distinguish the two syntaxes.
    232232Matita's syntax is largely straightforward to those familiar with Coq or O'Caml.
    233 The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically, if possible.
     233The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically.
    234234
    235235\subsection{Development strategy}
     
    250250% SECTION                                                                      %
    251251%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    252 \subsection{Representation of integers}
     252\subsection{Representation of bytes, words, etc.}
    253253\label{subsect.representation.integers}
    254254
     
    258258\begin{lstlisting}
    259259type 'a vect = bit list
    260 type word = [`Sixteen] vect
     260type nibble = [`Sixteen] vect
    261261type byte = [`Eight] vect
    262 $\color{blue}{\mathtt{let}}$ from_nibble =
    263  function
    264     [b1;b2;b3;b4] -> b1,b2,b3,b4
    265   | _ -> assert false
     262$\color{blue}{\mathtt{let}}$ split_word w = split_nth 4 w
     263$\color{blue}{\mathtt{let}}$ split_byte b = split_nth 2 b
    266264\end{lstlisting}
    267265\end{minipage}
     
    273271type word = [`Sixteen] vect
    274272type byte = [`Eight] vect
    275 val from_nibble: nibble -> bit*bit*bit*bit
     273val split_word: word -> byte * word
     274val split_byte: byte -> nibble * nibble
    276275\end{lstlisting}
    277276\end{minipage}
     
    280279\end{figure}
    281280
    282 Integers are represented using bitvectors, i.e. fixed length vectors of booleans.
    283 In our O'Caml emulator, we `faked' bitvectors using phantom types and polymorphic variants, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
    284 From within the bitvector module (left column) bitvectors are just lists of bits.
    285 However, the module's interface (right column) hides this implementation completely.
    286 
    287 In Matita, we are able to use the full power of dependent types to define `real' bitvectors:
     281The 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.
     282In 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}.
     283From 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.
     284
     285In Matita, we are able to use the full power of dependent types to always work with vectors of a known size:
    288286\begin{lstlisting}
    289287inductive Vector (A: Type[0]): nat → Type[0] ≝
     
    292290\end{lstlisting}
    293291We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}.
    294 We may use Matita's type system to provide even stronger guarantees, here on a function that splits a vector into two pieces at any index, providing that the index is smaller than the length of the \texttt{Vector} to be split:
     292We may use Matita's type system to provide precise typing for functions that are
     293polymorphic in the size without having to duplicate the code as we did in O'Caml:
    295294\begin{lstlisting}
    296295let rec split (A: Type[0]) (m,n: nat) on m:
Note: See TracChangeset for help on using the changeset viewer.