Changeset 540


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

Added appendix with main functions

File:
1 edited

Legend:

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

    r539 r540  
    223223\label{sect.design.issues.formalisation}
    224224
    225 From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similar syntaxes.
    226 Matita's syntax is similar to that of O'Caml.
    227 The only subtlety is the use of \texttt{?} in an argument position, which denotes an argument that should be inferred automatically, if possible.
     225From hereonin, we typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}} to distinguish the two syntaxes.
     226Matita's syntax is largely straightforward to those familiar with Coq or O'Caml.
     227The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically, if possible.
    228228
    229229\subsection{Development strategy}
     
    755755\label{sect.conclusions}
    756756
     757\newpage
     758
     759\appendix
     760
     761\section{Listing of main O'Caml functions}
     762\label{sect.listing.main.ocaml.functions}
     763
     764\subsubsection{From \texttt{ASMInterpret.ml(i)}}
     765
     766\begin{center}
     767\begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
     768Name & Description \\
     769\hline
     770\texttt{assembly} & Assembles an abstract syntax tree representing an 8051 assembly program into a list of bytes, its compiled form. \\
     771\texttt{initialize} & Initializes the emulator status. \\
     772\texttt{load} & Loads an assembled program into the emulator's code memory. \\
     773\texttt{fetch} & Fetches the next instruction, and automatically increments the program counter. \\
     774\texttt{execute} & Emulates the processor.  Accepts as input a function that pretty prints the emulator status after every emulation loop. \\
     775\end{tabular*}
     776\end{center}
     777
     778\subsubsection{From \texttt{IntelHex.ml(i)}}
     779
     780\begin{center}
     781\begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
     782Name & Description \\
     783\hline
     784\texttt{intel\_hex\_of\_file} & Reads in a file and parses it if in Intel IHX format, otherwise raises an exception. \\
     785\texttt{process\_intel\_hex} & Accepts a parsed Intel IHX file and populates a hashmap (of the same type as code memory) with the contents.
     786\end{tabular*}
     787\end{center}
     788
     789\subsubsection{From \texttt{Physical.ml(i)}}
     790
     791\begin{center}
     792\begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
     793Name & Description \\
     794\hline
     795\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. \\
     796\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. \\
     797\texttt{dec} & Decrements an eight bit bitvector with underflow, if necessary. \\
     798\texttt{inc} & Increments an eight bit bitvector with overflow, if necessary.
     799\end{tabular*}
     800\end{center}
     801
     802\newpage
     803
     804\section{Listing of main Matita functions}
     805\label{sect.listing.main.matita.functions}
     806
     807\subsubsection{From \texttt{Arithmetic.ma}}
     808
     809\begin{center}
     810\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
     811Title & Description \\
     812\hline
     813\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. \\
     814\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. \\
     815\texttt{half\_add} & Performs a standard half addition on bitvectors, returning the result and carry bit. \\
     816\texttt{full\_add} & Performs a standard full addition on bitvectors and a carry bit, returning the result and a carry bit.
     817\end{tabular*}
     818\end{center}
     819
     820\subsubsection{From \texttt{Assembly.ma}}
     821
     822\begin{center}
     823\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
     824Title & Description \\
     825\hline
     826\texttt{assemble1} & Assembles a single 8051 assembly instruction into its memory representation. \\
     827\texttt{assemble} & Assembles an 8051 assembly program into its memory representation.\\
     828\texttt{assemble\_unlabelled\_program} &\\& Assembles a list of (unlabelled) 8051 assembly instructions into its memory representation.
     829\end{tabular*}
     830\end{center}
     831
     832\subsubsection{From \texttt{BitVectorTrie.ma}}
     833
     834\begin{center}
     835\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
     836Title & Description \\
     837\hline
     838\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. \\
     839\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.
     840\end{tabular*}
     841\end{center}
     842
     843\subsubsection{From \texttt{DoTest.ma}}
     844
     845\begin{center}
     846\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
     847Title & Description \\
     848\hline
     849\texttt{execute\_trace} & Executes an assembly program for a fixed number of steps, recording in a trace which instructions were executed.
     850\end{tabular*}
     851\end{center}
     852
     853\subsubsection{From \texttt{Fetch.ma}}
     854
     855\begin{center}
     856\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
     857Title & Description \\
     858\hline
     859\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. \\
     860\end{tabular*}
     861\end{center}
     862
     863\subsubsection{From \texttt{Interpret.ma}}
     864
     865\begin{center}
     866\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
     867Title & Description \\
     868\hline
     869\texttt{execute\_1} & Executes a single step of an 8051 assembly program. \\
     870\texttt{execute} & Executes a fixed number of steps of an 8051 assembly program.
     871\end{tabular*}
     872\end{center}
     873
     874\subsubsection{From \texttt{Status.ma}}
     875
     876\begin{center}
     877\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
     878Title & Description \\
     879\hline
     880\texttt{load} & Loads an assembled 8051 assembly program into code memory.
     881\end{tabular*}
     882\end{center}
     883
    757884\end{document}
Note: See TracChangeset for help on using the changeset viewer.