Changeset 423 for Deliverables


Ignore:
Timestamp:
Dec 14, 2010, 4:49:35 PM (9 years ago)
Author:
mulligan
Message:

Discussed partiality in the case of assembly: use of Maybe monad.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Report/report.tex

    r422 r423  
    405405\item
    406406\textbf{Assert false} may be called is some feature of the physical 8051 processor is not implemented in the O'Caml emulator and an executing program is attempting to use it.
     407\item
     408\textbf{Assert false} may be called when the real, physical processor's behaviour would be undefined.
     409An example of this is loading a program which is too large for the available amount of code memory that the processor provides.
    407410\end{enumerate}
    408411
    409 The three manifestations of partiality above can be split into two types: partiality that manifests itself due to O'Caml's type system not being strong enough to rule the cause out, and partiality that signals a `real' crash in the processor due to the user attempting to use an unimplemented feature.
    410 Items 1 and 2 belong to the former class, Item 3 to the latter.
     412The four manifestations of partiality above can be split into two types: partiality that manifests itself due to O'Caml's type system not being strong enough to rule the cause out, and partiality that signals a `real' crash in the processor due to the user attempting to use an unimplemented feature.
     413Items 1 and 2 belong to the former class, Items 3 and 4 to the latter.
    411414
    412415Clearly Items 1 and 2 above must be addressed in the Matita formalisation.
     
    421424When the emulator attempts to use an unimplemented feature, we introduce a metavariable, corresponding to an open proof obligation.
    422425These obligations are closed by performing a case analysis over \texttt{not\_implemented}.
     426
     427In the rare case that Item 4 is encountered (only once in the emulator, in the \texttt{assembly} function), we use the Maybe monad to signal failure or success.
    423428
    424429\subsection{Addressing modes: use of dependent types}
     
    662667\hline
    663668\texttt{assemble1} & Assembles a single 8051 assembly instruction into its encoded counterpart. \\
    664 \texttt{assemble} & Assembles a list of 8051 assembly instructions into their encoded counterpart.
     669\texttt{assemble} & Assembles a list of 8051 assembly pseudo-instructions into their encoded counterpart.
    665670\end{tabular*}
    666671\end{center}
Note: See TracChangeset for help on using the changeset viewer.