\documentclass[times]{article} \usepackage{vdmlisting} \usepackage{hyperref} \usepackage{vdm} \def\vdmlisting{\texttt{vdmlisting}} \def\envvdmsl{\texttt{vdmsl}} \def\envvdmpp{\texttt{vdmpp}} \def\envvdmrt{\texttt{vdmrt}} \title{The \textbf{\vdmlisting} Package} \author{Kenneth Lausdahl\\ Dept. of Engineering\\ Aarhus University\\ Denmark.\\ \texttt{lausdahl@cs.au.dk}} \date{10 April 2013 \\ Version 1.0} \begin{document} \maketitle \begin{abstract} The \vdmlisting package is a Vienna Development Method (VDM) source code printer for \LaTeX . The package uses the listings package and provides a number of new listing environments for the three VDM dialects: VDM-SL,VDM-PP and VDM-RT. If one wants to typeset VDM with a mathematical syntax instead of the ASCII syntax used here then use the \texttt{vdm} package instead. \end{abstract} \tableofcontents \section{Getting started} Before using the \vdmlisting package, you should be familiar with the \LaTeX typesetting system and the listings package which this packages depends upon. \subsection{A minimal example} Here is a minimal file for \vdmlisting showing a VDM function: \begin{verbatim} \documentstyle{article} \usepackage{vdmlisting} \begin{document} \begin{vdmsl} add : int * int -> add(a,b) == a+b; \end{vdmsl} \end{document} \end{verbatim} \subsection{Typesetting VDM with listings} This package defined three listing environments that can be used to typeset VDM. The environments are defined as: \begin{verbatim} \begin{listing-name}[options] VDM specification \end{listing-name} \end{verbatim} \noindent The \texttt{options} are parsed directly to the \texttt{lstlisting} environment and could be used to e.g. set the label or caption like \texttt{label=lst:mymodel,caption=My special specification}. The \texttt{listing-name} may be any of the following: \begin{description} \item[\envvdmsl] The \envvdmsl environment configures the listing environment to use the VDM-SL language definition: \begin{verbatim} \begin{vdmsl}[label=lst:mymodule,caption=My module] module MyModule end MyModule \end{vdmsl} \end{verbatim} it typesets as follows: \begin{vdmsl}[label=lst:mymodule,caption=My module] module MyModule end MyModule \end{vdmsl} \item[\envvdmpp] The \envvdmpp environment configures the listing environment to use the VDM-PP language definition: \begin{verbatim} \begin{vdmpp}[label=lst:myclass,caption=My Class] class MyClass end MyClass \end{vdmpp} \end{verbatim} it typesets as follows: \begin{vdmpp}[label=lst:myclass,caption=My Class] class MyClass end MyClass \end{vdmpp} \item[\envvdmrt] The \envvdmrt environment configures the listing environment to use the VDM-RT language definition: \begin{verbatim} \begin{vdmrt}[label=lst:myclass,caption=My System] system MySystem end MySystem \end{vdmrt} \end{verbatim} it typesets as follows: \begin{vdmrt}[label=lst:myclass,caption=My System] system MySystem end MySystem \end{vdmrt} \end{description} Furthermore, the environments are configured with \texttt{escapeinside=\{(*@\}\{@*)\}} enabling the command \texttt{\textbackslash vdmnotcovered\{ VDM specification\}} to be used to mark execution coverage for the VDM specification displayed. \section{Package loading} As usual in \LaTeX, the package is loaded by \texttt{\textbackslash usepackage[optionsi]\{vdmlisting\}}, where [optionsi] is optional and gives a comma separated list of options: \begin{description} \item[color] This loads the \texttt{color} package and defines the \texttt{vdmnotcovered} command to use a red color. \item[notimes] This package loads the \texttt{times} package, by default, so if you do not want that to happen use this option to skip the load of \texttt{times}. \end{description} \section{Installing the \vdmlisting \ files} Place the file {\tt vdmlisting.sty} in your standard directory for \LaTeX\ style files (your system administrator will know where this is). \section{The License} The vdmlisting.sty and vdmlisting.tex file is copyright 2012--2013 Kenneth Lausdahl and is released under the LaTeX Project Public License 1.3 or later. \end{document}