Changeset 527


Ignore:
Timestamp:
Feb 16, 2011, 11:08:15 AM (6 years ago)
Author:
mulligan
Message:

added section on representation of integers

File:
1 edited

Legend:

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

    r526 r527  
    3232  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on},
    3333   morekeywords={[2]whd,normalize,elim,cases,destruct},
    34    morekeywords={[3]type,ofm},
     34   morekeywords={[3]type,of,val},
    3535   mathescape=true,
    3636  }
     
    4949\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
    5050
    51 \author{Claudio Sacerdoti Coen \and Dominic P. Mulligan}
    52 \authorrunning{C. Sacerdoti Coen and D. P. Mulligan}
     51% Who is first author?  Is CSC classed as a `S', or as a `C'?
     52\author{Dominic P. Mulligan \and Claudio Sacerdoti Coen}
     53\authorrunning{D. P. Mulligan and C. Sacerdoti Coen}
    5354\title{An executable formalisation of the MCS-51 microprocessor in Matita}
    5455\titlerunning{An executable formalisation of the MCS-51}
     
    218219% SECTION                                                                      %
    219220%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    220 \section{From O'Caml prototype to Matita formalisation}
    221 \label{sect.from.o'caml.prototype.matita.formalisation}
     221\section{Design issues in the formalisation}
     222\label{sect.design.issues.formalisation}
     223
     224From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes.
     225
     226\subsection{Development strategy}
     227\label{subsect.development.strategy}
    222228
    223229Our implementation progressed in two stages:
     
    238244% SECTION                                                                      %
    239245%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    240 \section{Design issues in the formalisation}
    241 \label{sect.design.issues.formalisation}
    242 
    243 From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes.
    244 
    245 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    246 % SECTION                                                                      %
    247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    248246\subsection{Representation of integers}
    249247\label{subsect.representation.integers}
     248
     249Integers are represented using bitvectors, i.e. fixed length vectors of booleans.
     250In our O'Caml emulator, we `faked' bitvectors using phantom types and polymorphic variants, like so:
     251\begin{lstlisting}
     252type bit = bool
     253type 'a vect = bit list
     254type word = [`Sixteen] vect
     255type byte = [`Eight] vect
     256\end{lstlisting}
     257Using this technique, we can provide precise typings for utility and arithmetic functions giving us some stronger guarantees of type safety.
     258For instance, functions that split \texttt{word}s into their constituent \texttt{byte}s:
     259\begin{lstlisting}
     260val from_word: word -> byte * byte
     261\end{lstlisting}
     262In Matita, we are able to use the full power of dependent types to define `real' bitvectors:
     263\begin{lstlisting}
     264inductive Vector (A: Type[0]): nat → Type[0] ≝
     265  VEmpty: Vector A O
     266| VCons: ∀n: nat. A → Vector A n → Vector A (S n).
     267\end{lstlisting}
     268We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}.
     269We 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:
     270\begin{lstlisting}
     271let rec split (A: Type[0]) (m,n: nat) on m:
     272   Vector A (plus m n) $\rightarrow$ (Vector A m) $\times$ (Vector A n) := ...
     273\end{lstlisting}
    250274
    251275%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.