Changeset 540 for Deliverables/D4.1/ITPPaper/itp2011.tex
 Timestamp:
 Feb 16, 2011, 5:21:03 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.tex
r539 r540 223 223 \label{sect.design.issues.formalisation} 224 224 225 From hereonin, we typeset O'Caml source with blue and Matita source with red to distinguish between the two similarsyntaxes.226 Matita's syntax is similar to that ofO'Caml.227 The only subtlety is the use of \texttt{?} in an argument position, which denotesan argument that should be inferred automatically, if possible.225 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. 226 Matita's syntax is largely straightforward to those familiar with Coq or O'Caml. 227 The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically, if possible. 228 228 229 229 \subsection{Development strategy} … … 755 755 \label{sect.conclusions} 756 756 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}} 768 Name & 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}} 782 Name & 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}} 793 Name & 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}} 811 Title & 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}} 824 Title & 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}} 836 Title & 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}} 847 Title & 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}} 857 Title & 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}} 867 Title & 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}} 878 Title & Description \\ 879 \hline 880 \texttt{load} & Loads an assembled 8051 assembly program into code memory. 881 \end{tabular*} 882 \end{center} 883 757 884 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.