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

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

...

File:
1 edited

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

 r553 From hereonin, we typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}} to distinguish the two syntaxes. 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, if possible. The only subtlety is the use of \texttt{?}' in an argument position denoting an argument that should be inferred automatically. \subsection{Development strategy} % SECTION                                                                      % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \subsection{Representation of integers} \subsection{Representation of bytes, words, etc.} \label{subsect.representation.integers} \begin{lstlisting} type 'a vect = bit list type word = [Sixteen] vect type nibble = [Sixteen] vect type byte = [Eight] vect $\color{blue}{\mathtt{let}}$ from_nibble = function [b1;b2;b3;b4] -> b1,b2,b3,b4 | _ -> assert false $\color{blue}{\mathtt{let}}$ split_word w = split_nth 4 w $\color{blue}{\mathtt{let}}$ split_byte b = split_nth 2 b \end{lstlisting} \end{minipage} type word = [Sixteen] vect type byte = [Eight] vect val from_nibble: nibble -> bit*bit*bit*bit val split_word: word -> byte * word val split_byte: byte -> nibble * nibble \end{lstlisting} \end{minipage} \end{figure} Integers are represented using bitvectors, i.e. fixed length vectors of booleans. In our O'Caml emulator, we faked' bitvectors using phantom types and polymorphic variants, as in Figure~\ref{fig.ocaml.implementation.bitvectors}. From within the bitvector module (left column) bitvectors are just lists of bits. However, the module's interface (right column) hides this implementation completely. In Matita, we are able to use the full power of dependent types to define real' bitvectors: 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}. 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. In Matita, we are able to use the full power of dependent types to always work with vectors of a known size: \begin{lstlisting} inductive Vector (A: Type[0]): nat → Type[0] ≝ \end{lstlisting} We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}. 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: We may use Matita's type system to provide precise typing for functions that are polymorphic in the size without having to duplicate the code as we did in O'Caml: \begin{lstlisting} let rec split (A: Type[0]) (m,n: nat) on m:
Note: See TracChangeset for help on using the changeset viewer.