manual.tex 2.13 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
doc  
MARCHE Claude committed
79
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
80 81 82

\input{ide.tex}

MARCHE Claude's avatar
docs  
MARCHE Claude committed
83 84
\input{library.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}

Andrei Paskevich's avatar
Andrei Paskevich committed
89 90
\input{glossary.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
91 92
\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
93
\chapter{Complete API documentation}
MARCHE Claude's avatar
MARCHE Claude committed
94
\label{chap:apidoc}
MARCHE Claude's avatar
MARCHE Claude committed
95 96 97

\input{./apidoc.tex}

MARCHE Claude's avatar
MARCHE Claude committed
98
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
99 100
\bibliography{manual}
%\input{biblio-demons}
101

MARCHE Claude's avatar
MARCHE Claude committed
102
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
103 104 105 106 107 108

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