manual.tex 1.87 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
MARCHE Claude committed
71 72
\input{intro.tex}

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

\input{ide.tex}

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

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
81
\chapter{Complete API documentation}
MARCHE Claude's avatar
MARCHE Claude committed
82
\label{chap:apidoc}
MARCHE Claude's avatar
MARCHE Claude committed
83 84 85

\input{./apidoc.tex}

MARCHE Claude's avatar
MARCHE Claude committed
86 87 88
\bibliographystyle{abbrv}
\bibliography{manual}

MARCHE Claude's avatar
MARCHE Claude committed
89
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
90 91 92 93 94 95

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