Add more to the example

1 files changed, 6 insertions, 6 deletions

diff --git a/algorithm.tex b/algorithm.tex
index 7d119da..31bf6bb 100644
--- a/algorithm.tex
+++ b/algorithm.tex
@@ -46,10 +46,10 @@ int main() {
 }
 \end{minted}
   \end{minipage}
-  \caption{Matrix multiply example C code.}\label{fig:matrix_mult_c}
+  \caption{Accumulator example C code.}\label{fig:accumulator_c}
 \end{figure}
 
-To describe the translation, we start with an example of how to translate a simple accumulator example, which is shown in figure~\ref{fig:matrix_mult_c}.
+To describe the translation, we start with an example of how to translate a simple accumulator example, which is shown in figure~\ref{fig:accumulator_c}.  Using this example, the different stages in the translation can be explained, together with how they were proven.  The example includes constructs such as arrays, for loops and addition, however, CoqUp also supports all other operators like multiplication and division, as well as conditional statements.  Function calls are also supported by inlining all of the functions, meaning recursive function calls are not supported.
 
 \subsection{CompCert RTL}
 
@@ -61,6 +61,8 @@ All CompCert intermediate language follow the similar structure below:
                  &\mathbf{main} : \mathit{id} \}
 \end{align*}
 
+\noindent where function definitions can either be internal or external.  External functions are functions that are not defined in the current translation unit, and are therefore not part of the current translation.  The difference in between the CompCert intermediate languages is therefore how the internal function is defined, as that defines the structure of the language itself.
+
 \begin{figure}
   \centering
   \begin{minipage}{0.5\linewidth}
@@ -88,13 +90,11 @@ main() {
 }
 \end{minted}
   \end{minipage}
-  \caption{Matrix multiply example C code.}\label{fig:matrix_mult_rtl}
+  \caption{Accumulator example RTL code.}\label{fig:accumulator_rtl}
 \end{figure}
 
-\noindent where function definitions can either be internal or external.  External functions are functions that are not defined in the current translation unit, and are therefore not part of the current translation.  The difference in between the CompCert intermediate languages is therefore how the internal function is defined, as that defines the structure of the language itself.
-
 %% Describe RTL
-RTL function definitions are a sequence of instructions encoded in a control-flow graph, with each instruction linking to the next instruction that should be executed.
+The accumulator example in RTL function definitions are a sequence of instructions encoded in a control-flow graph, with each instruction linking to the next instruction that should be executed.
 
 %%TODO: Finish this section and describe the syntax and semantics of RTL.