manual.tex 2.06 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
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
14 15
\sloppy
\hbadness=1100
MARCHE Claude's avatar
MARCHE Claude committed
16

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

\cleardoublepage

\tableofcontents

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

\section*{Acknowledgements}

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

MARCHE Claude's avatar
MARCHE Claude committed
74 75
\input{intro.tex}

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

\input{ide.tex}

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

\input{whyml.tex}

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

\input{manpages.tex}

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

\input{./apidoc.tex}

MARCHE Claude's avatar
MARCHE Claude committed
93
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
94 95
\bibliography{manual}
%\input{biblio-demons}
96

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

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