Changeset 527
 Timestamp:
 Feb 16, 2011, 11:08:15 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.tex
r526 r527 32 32 {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on}, 33 33 morekeywords={[2]whd,normalize,elim,cases,destruct}, 34 morekeywords={[3]type,of m},34 morekeywords={[3]type,of,val}, 35 35 mathescape=true, 36 36 } … … 49 49 \DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}} 50 50 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} 53 54 \title{An executable formalisation of the MCS51 microprocessor in Matita} 54 55 \titlerunning{An executable formalisation of the MCS51} … … 218 219 % SECTION % 219 220 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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 224 From 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} 222 228 223 229 Our implementation progressed in two stages: … … 238 244 % SECTION % 239 245 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%248 246 \subsection{Representation of integers} 249 247 \label{subsect.representation.integers} 248 249 Integers are represented using bitvectors, i.e. fixed length vectors of booleans. 250 In our O'Caml emulator, we `faked' bitvectors using phantom types and polymorphic variants, like so: 251 \begin{lstlisting} 252 type bit = bool 253 type 'a vect = bit list 254 type word = [`Sixteen] vect 255 type byte = [`Eight] vect 256 \end{lstlisting} 257 Using this technique, we can provide precise typings for utility and arithmetic functions giving us some stronger guarantees of type safety. 258 For instance, functions that split \texttt{word}s into their constituent \texttt{byte}s: 259 \begin{lstlisting} 260 val from_word: word > byte * byte 261 \end{lstlisting} 262 In Matita, we are able to use the full power of dependent types to define `real' bitvectors: 263 \begin{lstlisting} 264 inductive 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} 268 We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}. 269 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: 270 \begin{lstlisting} 271 let 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} 250 274 251 275 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset
for help on using the changeset viewer.