extraction-example.tex

\chapter{Textual BON Extraction Example}
In this appendix is an example of textual \bon{} extracted from Eiffel. The class in question is the \textsc{mml$\_$model} class from the EiffelBase2 library. Both informal and formal \bon are included. The formal \bon{} specification starts on line 280 of the extracted textual \bon{}. Eiffel and textual \bon{} can also be found on the attached \textsc{cd}. Lastly, small $\cup$'s seemed to have sneaked their way in during the \LaTeX{} formatting. These are not present in the extracted \bon{} and should be replaced with spaces.
\section{Eiffel Source Code}
\label{appendix-bon-extraction-example}
\lstset{
basicstyle=\ttfamily\scriptsize,
language=Eiffel,
numbers=left
}
\lstinputlisting{MML_MODEL.e}
\break
\section{Extracted BON}
\lstset{
basicstyle=\ttfamily\scriptsize,
numbers=left
}
\lstinputlisting{MML_MODEL.bon}