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