# Changeset 423

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

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

File:
1 edited

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

 r422 \item \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. \item \textbf{Assert false} may be called when the real, physical processor's behaviour would be undefined. An example of this is loading a program which is too large for the available amount of code memory that the processor provides. \end{enumerate} 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. Items 1 and 2 belong to the former class, Item 3 to the latter. The 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. Items 1 and 2 belong to the former class, Items 3 and 4 to the latter. Clearly Items 1 and 2 above must be addressed in the Matita formalisation. When the emulator attempts to use an unimplemented feature, we introduce a metavariable, corresponding to an open proof obligation. These obligations are closed by performing a case analysis over \texttt{not\_implemented}. In 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. \subsection{Addressing modes: use of dependent types} \hline \texttt{assemble1} & Assembles a single 8051 assembly instruction into its encoded counterpart. \\ \texttt{assemble} & Assembles a list of 8051 assembly instructions into their encoded counterpart. \texttt{assemble} & Assembles a list of 8051 assembly pseudo-instructions into their encoded counterpart. \end{tabular*} \end{center}
Note: See TracChangeset for help on using the changeset viewer.