manual.tex 3.34 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
\usepackage{graphicx}
MARCHE Claude's avatar
MARCHE Claude committed
7

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
11 12
% for ocamldoc generated pages
\usepackage{ocamldoc}
MARCHE Claude's avatar
MARCHE Claude committed
13 14
\let\tt\ttfamily
\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
15

MARCHE Claude's avatar
MARCHE Claude committed
16 17
\usepackage{ifthen}
\input{./macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
18

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

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

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

\begin{center}

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

\vfill

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

\vfill

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

\vfill

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

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
47 48 49 50 51 52 53 54 55 56 57 58
\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
59 60 61
\begin{tabular}{l}
$^1$ Univ Paris-Sud, Orsay, F-91405 \\
$^2$ LRI, CNRS, Orsay, F-91405 \\
Andrei Paskevich's avatar
Andrei Paskevich committed
62
$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
63 64
\end{tabular}

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

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

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

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


MARCHE Claude's avatar
MARCHE Claude committed
89 90 91 92 93 94 95 96 97 98
\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
MARCHE Claude's avatar
MARCHE Claude committed
99
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
100 101 102 103 104 105 106 107 108 109 110
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
111
\section*{Acknowledgements}
MARCHE Claude's avatar
MARCHE Claude committed
112

MARCHE Claude's avatar
MARCHE Claude committed
113 114
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
115 116 117 118 119

\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
120

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

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

MARCHE Claude's avatar
MARCHE Claude committed
125 126
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
127
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
128

MARCHE Claude's avatar
MARCHE Claude committed
129
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
130

MARCHE Claude's avatar
MARCHE Claude committed
131
% \input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
132

MARCHE Claude's avatar
doc  
MARCHE Claude committed
133 134
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
135 136
\part{Reference Manual}

137
% \input{glossary.tex}
Andrei Paskevich's avatar
Andrei Paskevich committed
138

MARCHE Claude's avatar
MARCHE Claude committed
139 140 141 142
\input{syntaxref.tex}

\input{library.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
143 144
\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
145
\chapter{Complete API documentation}
MARCHE Claude's avatar
MARCHE Claude committed
146
\label{chap:apidoc}
MARCHE Claude's avatar
MARCHE Claude committed
147 148 149

\input{./apidoc.tex}

MARCHE Claude's avatar
MARCHE Claude committed
150
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
151 152
\bibliography{manual}
%\input{biblio-demons}
153

MARCHE Claude's avatar
MARCHE Claude committed
154
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
155 156 157 158 159 160

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