Changeset 517


Ignore:
Timestamp:
Feb 15, 2011, 2:53:35 PM (6 years ago)
Author:
mulligan
Message:

more added

File:
1 edited

Legend:

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

    r516 r517  
    218218% SECTION                                                                      %
    219219%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    220 \subsection{Emulator architecture}
    221 \label{subsect.emulator.architecture}
    222 
    223 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    224 % SECTION                                                                      %
    225 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    226220\section{From O'Caml prototype to Matita formalisation}
    227221\label{sect.from.o'caml.prototype.matita.formalisation}
     
    245239%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    246240\section{Design issues in the formalisation}
    247 \label{sect.design.issues.formalisation}
     241\label{sect.design.issues.formalisation}
     242
     243From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes.
    248244
    249245%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    299295% SECTION                                                                      %
    300296%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    301 \subsection{Putting dependent types to work}
    302 \label{subsect.putting.dependent.types.to.work}
    303 
    304 We typeset O'Caml source with blue, and Matita source with red.
     297\subsection{Emulator architecture}
     298\label{subsect.emulator.architecture}
     299
     300The internal state of our Matita emulator is represented as a record:
     301\begin{quote}
     302\begin{lstlisting}
     303record Status: Type[0] ≝
     304{
     305  code_memory: BitVectorTrie Byte 16;
     306  low_internal_ram: BitVectorTrie Byte 7;
     307  high_internal_ram: BitVectorTrie Byte 7;
     308  external_ram: BitVectorTrie Byte 16;
     309  program_counter: Word;
     310  special_function_registers_8051: Vector Byte 19;
     311  special_function_registers_8052: Vector Byte 5;
     312  ...
     313}.
     314\end{lstlisting}
     315\end{quote}
     316This record neatly encapsulates the current memory contents, the program counter, the state of the current SFRs, and so on.
     317One peculiarity is the packing of the 24 combined SFRs into fixed length vectors.
     318This was due to a bug in Matita when we were constructing the emulator, since fixed, where the time needed to typecheck a record grew exponentially with the number of fields.
     319
     320
     321
     322%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     323% SECTION                                                                      %
     324%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     325\subsection{Instruction set unorthogonality}
     326\label{subsect.instruction.set.unorthogonality}
    305327
    306328A peculiarity of the MCS-51 is the non-orthogonality of its instruction set.
Note: See TracChangeset for help on using the changeset viewer.