# Changeset 540 for Deliverables/D4.1/ITP-Paper/itp-2011.tex

Ignore:
Timestamp:
Feb 16, 2011, 5:21:03 PM (9 years ago)
Message:

 r539 \label{sect.design.issues.formalisation} From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes. Matita's syntax is similar to that of O'Caml. The only subtlety is the use of \texttt{?} in an argument position, which denotes an argument that should be inferred automatically, if possible. From hereonin, we typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}} to distinguish the two syntaxes. Matita's syntax is largely straightforward to those familiar with Coq or O'Caml. The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically, if possible. \subsection{Development strategy} \label{sect.conclusions} \newpage \appendix \section{Listing of main O'Caml functions} \label{sect.listing.main.ocaml.functions} \subsubsection{From \texttt{ASMInterpret.ml(i)}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}} Name & Description \\ \hline \texttt{assembly} & Assembles an abstract syntax tree representing an 8051 assembly program into a list of bytes, its compiled form. \\ \texttt{initialize} & Initializes the emulator status. \\ \texttt{load} & Loads an assembled program into the emulator's code memory. \\ \texttt{fetch} & Fetches the next instruction, and automatically increments the program counter. \\ \texttt{execute} & Emulates the processor.  Accepts as input a function that pretty prints the emulator status after every emulation loop. \\ \end{tabular*} \end{center} \subsubsection{From \texttt{IntelHex.ml(i)}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}} Name & Description \\ \hline \texttt{intel\_hex\_of\_file} & Reads in a file and parses it if in Intel IHX format, otherwise raises an exception. \\ \texttt{process\_intel\_hex} & Accepts a parsed Intel IHX file and populates a hashmap (of the same type as code memory) with the contents. \end{tabular*} \end{center} \subsubsection{From \texttt{Physical.ml(i)}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}} Name & Description \\ \hline \texttt{subb8\_with\_c} & Performs an eight bit subtraction on bitvectors.  The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\ \texttt{add8\_with\_c} & Performs an eight bit addition on bitvectors.  The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\ \texttt{dec} & Decrements an eight bit bitvector with underflow, if necessary. \\ \texttt{inc} & Increments an eight bit bitvector with overflow, if necessary. \end{tabular*} \end{center} \newpage \section{Listing of main Matita functions} \label{sect.listing.main.matita.functions} \subsubsection{From \texttt{Arithmetic.ma}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}p{9cm}} Title & Description \\ \hline \texttt{add\_n\_with\_carry} & Performs an $n$ bit addition on bitvectors.  The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\ \texttt{sub\_8\_with\_carry} & Performs an eight bit subtraction on bitvectors. The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\ \texttt{half\_add} & Performs a standard half addition on bitvectors, returning the result and carry bit. \\ \texttt{full\_add} & Performs a standard full addition on bitvectors and a carry bit, returning the result and a carry bit. \end{tabular*} \end{center} \subsubsection{From \texttt{Assembly.ma}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}p{9cm}} Title & Description \\ \hline \texttt{assemble1} & Assembles a single 8051 assembly instruction into its memory representation. \\ \texttt{assemble} & Assembles an 8051 assembly program into its memory representation.\\ \texttt{assemble\_unlabelled\_program} &\\& Assembles a list of (unlabelled) 8051 assembly instructions into its memory representation. \end{tabular*} \end{center} \subsubsection{From \texttt{BitVectorTrie.ma}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}p{9cm}} Title & Description \\ \hline \texttt{lookup} & Returns the data stored at the end of a particular path (a bitvector) from the trie.  If no data exists, returns a default value. \\ \texttt{insert} & Inserts data into a tree at the end of the path (a bitvector) indicated.  Automatically expands the tree (by filling in stubs) if necessary. \end{tabular*} \end{center} \subsubsection{From \texttt{DoTest.ma}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}p{9cm}} Title & Description \\ \hline \texttt{execute\_trace} & Executes an assembly program for a fixed number of steps, recording in a trace which instructions were executed. \end{tabular*} \end{center} \subsubsection{From \texttt{Fetch.ma}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}p{9cm}} Title & Description \\ \hline \texttt{fetch} & Decodes and returns the instruction currently pointed to by the program counter and automatically increments the program counter the required amount to point to the next instruction. \\ \end{tabular*} \end{center} \subsubsection{From \texttt{Interpret.ma}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}p{9cm}} Title & Description \\ \hline \texttt{execute\_1} & Executes a single step of an 8051 assembly program. \\ \texttt{execute} & Executes a fixed number of steps of an 8051 assembly program. \end{tabular*} \end{center} \subsubsection{From \texttt{Status.ma}} \begin{center} \begin{tabular*}{\textwidth}{p{3cm}p{9cm}} Title & Description \\ \hline \texttt{load} & Loads an assembled 8051 assembly program into code memory. \end{tabular*} \end{center} \end{document}