manual.tex 1.83 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2
\documentclass[a4paper]{memoir}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
3
\usepackage[T1]{fontenc}
MARCHE Claude's avatar
MARCHE Claude committed
4
\usepackage{url}
MARCHE Claude's avatar
MARCHE Claude committed
5

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
6 7
% for ocamldoc generated pages
\usepackage{ocamldoc}
MARCHE Claude's avatar
MARCHE Claude committed
8 9
\let\tt\ttfamily
\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
10

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
11

MARCHE Claude's avatar
MARCHE Claude committed
12 13
\begin{document}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
\thispagestyle{empty}

\begin{center}

~

\vfill

{\Huge\bfseries Why3 manual}

\vfill

{\Large F. Bobot$^{1,2}$ \\ 
J.-C. Filli\^atre$^{2,1}$  \\ 
C. March\'e$^{3,1}$ \\ 
A. Paskevich$^{1,2}$}

\vfill

\begin{tabular}{l}
$^1$ Univ Paris-Sud, Orsay, F-91405 \\
$^2$ LRI, CNRS, Orsay, F-91405 \\
$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893 
\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
51 52 53 54 55

\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70
\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
external prover if wanted.  An major new feature is also the ability
to use Why programmatically, via an well-defined API.

\section*{Acknowledgements}

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

MARCHE Claude's avatar
doc  
MARCHE Claude committed
71
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
72 73 74

\input{ide.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
75 76 77 78
\input{api.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
79 80 81 82
\chapter{Complete API documentation}

\input{./apidoc.tex}

MARCHE Claude's avatar
MARCHE Claude committed
83 84 85
\bibliographystyle{abbrv}
\bibliography{manual}

MARCHE Claude's avatar
MARCHE Claude committed
86
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
87 88 89 90 91 92

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