Changeset 554
 Timestamp:
 Feb 17, 2011, 2:09:58 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.tex
r553 r554 231 231 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. 232 232 Matita'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.233 The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically. 234 234 235 235 \subsection{Development strategy} … … 250 250 % SECTION % 251 251 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 252 \subsection{Representation of integers}252 \subsection{Representation of bytes, words, etc.} 253 253 \label{subsect.representation.integers} 254 254 … … 258 258 \begin{lstlisting} 259 259 type 'a vect = bit list 260 type word= [`Sixteen] vect260 type nibble = [`Sixteen] vect 261 261 type 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 266 264 \end{lstlisting} 267 265 \end{minipage} … … 273 271 type word = [`Sixteen] vect 274 272 type byte = [`Eight] vect 275 val from_nibble: nibble > bit*bit*bit*bit 273 val split_word: word > byte * word 274 val split_byte: byte > nibble * nibble 276 275 \end{lstlisting} 277 276 \end{minipage} … … 280 279 \end{figure} 281 280 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: 281 The formalization of MCS51 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. 282 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}. 283 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. 284 285 In Matita, we are able to use the full power of dependent types to always work with vectors of a known size: 288 286 \begin{lstlisting} 289 287 inductive Vector (A: Type[0]): nat → Type[0] ≝ … … 292 290 \end{lstlisting} 293 291 We 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: 292 We may use Matita's type system to provide precise typing for functions that are 293 polymorphic in the size without having to duplicate the code as we did in O'Caml: 295 294 \begin{lstlisting} 296 295 let rec split (A: Type[0]) (m,n: nat) on m:
Note: See TracChangeset
for help on using the changeset viewer.