1\documentclass[12pt,a4paper]{report}
2
3\usepackage[a4paper,hscale=0.65,vscale=0.71]{geometry}
4
5\usepackage{isabelle,isabellesym}
6
7\usepackage{charter}
8
9\usepackage{tikz}
10\usetikzlibrary{shadows}
11
12\usepackage{listings}
13
14\usepackage{alltt}
15
16\usepackage{railsetup}
17
18% this should be the last package used
19\usepackage{pdfsetup}
20
21% urls in roman style, theory text in math-similar italics
22\urlstyle{rm}
23\isabellestyle{tt}
24
25\renewcommand{\isastyleminor}{\tt}
26
27\lstdefinelanguage{SPARK}[95]{Ada} {
28   morecomment=*[l]{--\#},
29   morekeywords=
30   {
31     inherit, own, initializes, hide, global, main_program,
32     derives, from, pre, post, return, assert, check
33   }
34}
35
36\lstset{ %
37language=SPARK,
38basicstyle=\small\ttfamily,
39keywordstyle=\rmfamily\bfseries,
40columns=flexible,
41showstringspaces=false
42}
43
44\newcommand{\mod}{\mathbin{\hbox{\textbf{mod}}}}
45
46\newcommand{\SPARK}{\textsc{Spark}}
47
48\newcommand{\secref}[1]{\S \ref{#1}}
49\newcommand{\figref}[1]{Fig.\ \ref{#1}}
50
51\renewcommand{\topfraction}{.99}
52\renewcommand{\bottomfraction}{.99}
53\setcounter{topnumber}{9}
54\setcounter{bottomnumber}{9}
55\setcounter{totalnumber}{20}
56
57
58\begin{document}
59
60\title{The HOL-\SPARK{} Program Verification Environment}
61\author{\emph{Stefan Berghofer} \\ \emph{secunet Security Networks AG}}
62\maketitle
63
64\tableofcontents
65
66% sane default for proof documents
67\parindent 0pt\parskip 0.5ex
68
69\input{intro}
70\input{Example_Verification}
71\input{VC_Principles}
72\input{Reference}
73
74% optional bibliography
75\bibliographystyle{abbrv}
76\bibliography{root}
77
78\end{document}
79
80%%% Local Variables:
81%%% mode: latex
82%%% TeX-master: t
83%%% End:
84