Commit 2ad0ce55 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

fix

parent 40956600
...@@ -237,6 +237,7 @@ val cf: cpu_flag ...@@ -237,6 +237,7 @@ val cf: cpu_flag
\end{verbatim} \end{verbatim}
Reasoning about the carry flag as an integer allows for the specification of the \texttt{ADD} Reasoning about the carry flag as an integer allows for the specification of the \texttt{ADD}
instruction as follows: instruction as follows:
\newpage
\begin{verbatim} \begin{verbatim}
val add (dst src: register): unit val add (dst src: register): unit
writes { cf, reg } writes { cf, reg }
...@@ -544,7 +545,7 @@ are modified by the code inside it, and are used to update the \emph{ghost regis ...@@ -544,7 +545,7 @@ are modified by the code inside it, and are used to update the \emph{ghost regis
\label{fig:abstractblock} \label{fig:abstractblock}
\end{figure} \end{figure}
In general, if assembly code is hand-written (or generated using a simple process), such information is expected to be available for In general, if assembly code is hand-written (or generated using a simple process), documentation is expected to be available for
complicated routines, and should be sufficient to inform a partitioning of it into abstract blocks. If assembly code is complicated routines, and should be sufficient to inform a partitioning of it into abstract blocks. If assembly code is
written with verification in mind, it should also be possible to instruct programmers to indicate potential blocks, written with verification in mind, it should also be possible to instruct programmers to indicate potential blocks,
or even to employ verification already during the development process. or even to employ verification already during the development process.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment