manual.tex 2.03 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

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
12

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
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 51
\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
52 53 54 55 56

\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
57 58 59 60 61 62 63 64
\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
65 66
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
67 68 69 70 71

\section*{Acknowledgements}

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

MARCHE Claude's avatar
MARCHE Claude committed
72 73
\input{intro.tex}

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

\input{ide.tex}

MARCHE Claude's avatar
docs  
MARCHE Claude committed
78 79 80 81
\input{library.tex}

\input{whyml.tex}

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

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
86
\chapter{Complete API documentation}
MARCHE Claude's avatar
MARCHE Claude committed
87
\label{chap:apidoc}
MARCHE Claude's avatar
MARCHE Claude committed
88 89 90

\input{./apidoc.tex}

MARCHE Claude's avatar
MARCHE Claude committed
91
\bibliographystyle{abbrv}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
92 93
%\bibliography{manual}
\input{biblio-demons}
94

MARCHE Claude's avatar
MARCHE Claude committed
95
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
96 97 98 99 100 101

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