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

7 8
%\usepackage[toc,nonumberlist]{glossaries}
%\makeglossaries
Andrei Paskevich's avatar
Andrei Paskevich committed
9

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

15 16
\newcommand{\why}{\textsf{Why3}}
\newcommand{\eg}{\emph{e.g.}}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
17

MARCHE Claude's avatar
MARCHE Claude committed
18 19
\input{./version.tex}

MARCHE Claude's avatar
MARCHE Claude committed
20
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
21 22
\sloppy
\hbadness=1100
MARCHE Claude's avatar
MARCHE Claude committed
23

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
24 25 26 27
\thispagestyle{empty}

\begin{center}

MARCHE Claude's avatar
MARCHE Claude committed
28 29 30 31 32
\rule\textwidth{0.8mm}

\vfill

{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
33 34 35

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
36
\rule\textwidth{0.8mm}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
37 38 39

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
40 41 42
\begin{LARGE}
  Version \whyversion{}, December 2010
\end{LARGE}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
43 44 45

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
46 47 48 49 50 51 52 53 54 55 56 57
\begin{Large}
  \begin{tabular}{c}
  Fran\c{c}ois Bobot$^{1}$ \\
  Jean-Christophe Filli\^atre$^{2}$  \\
  Claude March\'e$^{3}$ \\
  Andrei Paskevich$^{1}$
\end{tabular}
\end{Large}
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
58 59 60
\begin{tabular}{l}
$^1$ Univ Paris-Sud, Orsay, F-91405 \\
$^2$ LRI, CNRS, Orsay, F-91405 \\
Andrei Paskevich's avatar
Andrei Paskevich committed
61
$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
62 63
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
64
\bigskip
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
65

MARCHE Claude's avatar
MARCHE Claude committed
66
  \textcopyright 2010 Univ Paris-Sud, CNRS, INRIA
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
67

MARCHE Claude's avatar
MARCHE Claude committed
68
  This work has been partly supported by the `U3CAT' national ANR project
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
69 70 71 72 73 74
  (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
75

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
76 77 78 79 80 81 82 83
\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
84 85
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
86 87


MARCHE Claude's avatar
MARCHE Claude committed
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
\subsection*{Availability}

Why3 project page is \url{https://gforge.inria.fr/projects/why3}.  The
last distribution is available, in source format, together with this
documentation and several examples.

Why3 is distributed as open source and freely available under the
terms of the GNU LGPL 2.1. See the file \texttt{LICENSE}.

See the file \texttt{INSTALL} for quick installation instructions, and
Section~\ref{sec:install} od this document for more detailed
instructions.

\subsection*{Contact}

There is a public mailing list for users' discussions:
\url{http://lists.gforge.inria.fr/mailman/listinfo/why3-club}.

Report any bug to the Why3 Bug Tracking System:
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.


MARCHE Claude's avatar
MARCHE Claude committed
110
\section*{Acknowledgements}
MARCHE Claude's avatar
MARCHE Claude committed
111

MARCHE Claude's avatar
MARCHE Claude committed
112 113
We gratefully thank the people who contributed to Why3: Simon Cruanes,
Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.
MARCHE Claude's avatar
MARCHE Claude committed
114 115 116 117 118

\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
119

MARCHE Claude's avatar
MARCHE Claude committed
120 121
\input{intro.tex}

MARCHE Claude's avatar
MARCHE Claude committed
122 123
\part{Tutorial}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
124
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
125 126 127

\input{ide.tex}

MARCHE Claude's avatar
MARCHE Claude committed
128
% \input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
129

MARCHE Claude's avatar
doc  
MARCHE Claude committed
130 131
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
132 133
\part{Reference Manual}

134
% \input{glossary.tex}
Andrei Paskevich's avatar
Andrei Paskevich committed
135

MARCHE Claude's avatar
MARCHE Claude committed
136 137 138 139
\input{syntaxref.tex}

\input{library.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
140 141
\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
142
\chapter{Complete API documentation}
MARCHE Claude's avatar
MARCHE Claude committed
143
\label{chap:apidoc}
MARCHE Claude's avatar
MARCHE Claude committed
144 145 146

\input{./apidoc.tex}

MARCHE Claude's avatar
MARCHE Claude committed
147
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
148 149
\bibliography{manual}
%\input{biblio-demons}
150

MARCHE Claude's avatar
MARCHE Claude committed
151
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
152 153 154 155 156 157

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