manual.tex 2.2 KB
Newer Older
1
\documentclass[a4paper,11pt,twoside,openright]{memoir}
MARCHE Claude's avatar
MARCHE Claude committed
2

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
3
\usepackage[T1]{fontenc}
4 5
%\usepackage{url}
\usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
MARCHE Claude's avatar
MARCHE Claude committed
6

Andrei Paskevich's avatar
Andrei Paskevich committed
7 8 9
\usepackage[toc,nonumberlist]{glossaries}
\makeglossaries

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
10 11
% for ocamldoc generated pages
\usepackage{ocamldoc}
MARCHE Claude's avatar
MARCHE Claude committed
12 13
\let\tt\ttfamily
\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
14

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
15

MARCHE Claude's avatar
MARCHE Claude committed
16
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
17 18
\sloppy
\hbadness=1100
MARCHE Claude's avatar
MARCHE Claude committed
19

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
20 21 22 23 24 25 26 27 28 29 30 31
\thispagestyle{empty}

\begin{center}

~

\vfill

{\Huge\bfseries Why3 manual}

\vfill

Andrei Paskevich's avatar
Andrei Paskevich committed
32 33 34
{\Large F. Bobot$^{1,2}$ \\
J.-C. Filli\^atre$^{2,1}$  \\
C. March\'e$^{3,1}$ \\
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
35 36 37 38 39 40 41
A. Paskevich$^{1,2}$}

\vfill

\begin{tabular}{l}
$^1$ Univ Paris-Sud, Orsay, F-91405 \\
$^2$ LRI, CNRS, Orsay, F-91405 \\
Andrei Paskevich's avatar
Andrei Paskevich committed
42
$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56
\end{tabular}

\vfill

\begin{flushleft}
  \textcopyright 2010-2010 Univ Paris-Sud, CNRS, INRIA

  This work has been supported by the `U3CAT' national ANR project
  (ANR-08-SEGI-021-08, \url{http://frama-c.cea.fr/u3cat}) and by the
  Hi-Lite (\url{http://www.open-do.org/projects/hi-lite/}) FUI project of the
  System@tic competitivity cluster.

\end{flushleft}
\end{center}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
57 58 59 60 61

\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
62 63 64 65 66 67 68 69
\chapter*{Foreword}

This is the manual for the Why platform version 3, or Why3 for
short. Why3 is a complete reimplementation of the former Why
platform~\cite{filliatre07cav} for program verification.  The major
change is a completely new design of the architecture for calling
external provers. An important emphasis is put on the genericity,
which allows for the end user to easily add the support for a new
70 71
external prover if wanted.  A major new feature is also the ability
to use Why programmatically, via a well-designed API.
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
72 73 74 75 76

\section*{Acknowledgements}

We gratefully thank all the people who contributed to this document:

MARCHE Claude's avatar
MARCHE Claude committed
77 78
\input{intro.tex}

MARCHE Claude's avatar
MARCHE Claude committed
79 80
\part{Tutorial}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
81
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
82 83 84

\input{ide.tex}

MARCHE Claude's avatar
MARCHE Claude committed
85
% \input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
86

MARCHE Claude's avatar
doc  
MARCHE Claude committed
87 88
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
89 90
\part{Reference Manual}

Andrei Paskevich's avatar
Andrei Paskevich committed
91 92
\input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
93 94 95 96
\input{syntaxref.tex}

\input{library.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
97 98
\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
99
\chapter{Complete API documentation}
MARCHE Claude's avatar
MARCHE Claude committed
100
\label{chap:apidoc}
MARCHE Claude's avatar
MARCHE Claude committed
101 102 103

\input{./apidoc.tex}

MARCHE Claude's avatar
MARCHE Claude committed
104
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
105 106
\bibliography{manual}
%\input{biblio-demons}
107

MARCHE Claude's avatar
MARCHE Claude committed
108
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
109 110 111 112 113 114

%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: t
%%% End: