summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/vdmlisting/vdmlisting.tex
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/vdmlisting/vdmlisting.tex')
-rw-r--r--macros/latex/contrib/vdmlisting/vdmlisting.tex142
1 files changed, 142 insertions, 0 deletions
diff --git a/macros/latex/contrib/vdmlisting/vdmlisting.tex b/macros/latex/contrib/vdmlisting/vdmlisting.tex
new file mode 100644
index 0000000000..673b61a6aa
--- /dev/null
+++ b/macros/latex/contrib/vdmlisting/vdmlisting.tex
@@ -0,0 +1,142 @@
+
+
+\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}