manual.tex 6.46 KB
Newer Older
1
\documentclass[a4paper,11pt,twoside,openright]{memoir}
MARCHE Claude's avatar
MARCHE Claude committed
2

3 4
% rubber: module index

MARCHE Claude's avatar
MARCHE Claude committed
5 6 7
% tells memoir style to number subsections
\setsecnumdepth{subsection}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
8
\usepackage[T1]{fontenc}
9
\usepackage{lmodern}
10
%\usepackage{url}
11
\usepackage[pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
MARCHE Claude's avatar
MARCHE Claude committed
12
\usepackage{graphicx}
13
\usepackage{listings}
MARCHE Claude's avatar
MARCHE Claude committed
14
\usepackage{xspace}
MARCHE Claude's avatar
MARCHE Claude committed
15

MARCHE Claude's avatar
MARCHE Claude committed
16 17 18 19 20
\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
\setheadfoot{15pt}{38pt}
\checkandfixthelayout

MARCHE Claude's avatar
MARCHE Claude committed
21 22 23 24 25 26 27
% placement of figures
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}
\setcounter{topnumber}{4}
\setcounter{bottomnumber}{4}
\setcounter{totalnumber}{8}
MARCHE Claude's avatar
MARCHE Claude committed
28

MARCHE Claude's avatar
MARCHE Claude committed
29 30 31 32 33 34
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries

% \usepackage{glossary}
% \makeglossary
% \glossary{name={entry name}, description={entry description}}
Andrei Paskevich's avatar
Andrei Paskevich committed
35

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
36
% for ocamldoc generated pages
37
%\usepackage{ocamldoc}
MARCHE Claude's avatar
MARCHE Claude committed
38 39
\let\tt\ttfamily
\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
40

MARCHE Claude's avatar
MARCHE Claude committed
41 42
\usepackage{ifthen}
\input{./macros.tex}
43
\input{./replayer_macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
44

MARCHE Claude's avatar
MARCHE Claude committed
45 46
\input{./version.tex}

47 48
\makeindex

MARCHE Claude's avatar
MARCHE Claude committed
49
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
50
\sloppy
51
\hbadness=5000
MARCHE Claude's avatar
MARCHE Claude committed
52

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
53 54 55 56
\thispagestyle{empty}

\begin{center}

MARCHE Claude's avatar
MARCHE Claude committed
57 58 59 60 61
\rule\textwidth{0.8mm}

\vfill

{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
62 63 64

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
65
\rule\textwidth{0.8mm}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
66 67 68

\vfill

69
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
70 71


MARCHE Claude's avatar
MARCHE Claude committed
72
\begin{LARGE}
73
  Version \whyversion{}, May 2012
MARCHE Claude's avatar
MARCHE Claude committed
74
\end{LARGE}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
75 76 77

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
78 79
\begin{Large}
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
80 81 82
  Fran\c{c}ois Bobot$^{1,2}$ \\
  Jean-Christophe Filli\^atre$^{1,2}$  \\
  Claude March\'e$^{2,1}$ \\
83
  Guillaume Melquiond$^{2,1}$\\
MARCHE Claude's avatar
MARCHE Claude committed
84
  Andrei Paskevich$^{1,2}$
MARCHE Claude's avatar
MARCHE Claude committed
85 86 87 88 89 90
\end{tabular}
\end{Large}
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
91
\begin{tabular}{l}
MARCHE Claude's avatar
MARCHE Claude committed
92
$^1$ LRI, CNRS, Univ Paris-Sud, Orsay, F-91405 \\
Guillaume Melquiond's avatar
Guillaume Melquiond committed
93
$^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
94 95
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
96
\bigskip
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
97

98
  \textcopyright 2010-2012 Univ Paris-Sud, CNRS, INRIA
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
99

MARCHE Claude's avatar
MARCHE Claude committed
100
  This work has been partly supported by the `U3CAT' national ANR project
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
101 102 103 104 105 106
  (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
107

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
108 109
\chapter*{Foreword}

MARCHE Claude's avatar
MARCHE Claude committed
110
This is the manual for the Why platform version 3, or \why for
111 112 113 114 115 116 117 118
short. \why is a complete reimplementation~\cite{boogie11why3} of the former Why
platform~\cite{filliatre07cav} for program
verification. Among the new features are: numerous
extensions to the input language, a new architecture for calling
external provers, and a well-designed API, allowing to use \why as a
software library.  An important emphasis is put on modularity and
genericity, giving the end user a possibility to easily reuse \why
formalizations or to add support for a new external prover if wanted.
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
119

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
120
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
121

MARCHE Claude's avatar
MARCHE Claude committed
122 123 124
\why project page is \url{http://why3.lri.fr/}.  The last distribution
is available there, in source format, together with this documentation
and several examples.
MARCHE Claude's avatar
MARCHE Claude committed
125

MARCHE Claude's avatar
MARCHE Claude committed
126
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
127 128 129
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
130
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
131 132
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
133
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
134 135 136 137

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

MARCHE Claude's avatar
MARCHE Claude committed
138
Report any bug to the \why Bug Tracking System:
MARCHE Claude's avatar
MARCHE Claude committed
139 140 141
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.


Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
142
\subsection*{Acknowledgements}
MARCHE Claude's avatar
MARCHE Claude committed
143

MARCHE Claude's avatar
MARCHE Claude committed
144
We gratefully thank the people who contributed to \why, directly or
145 146
indirectly: Romain Bardou, Simon Cruanes, Leon Gondelman, Johannes Kanig,
St\'ephane Lescuyer, Sim\~ao Melo de Sousa, Benjamin Monate, Asma Tafat.
MARCHE Claude's avatar
MARCHE Claude committed
147

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
148
\subsection*{Summary of Changes w.r.t. Why 2}
MARCHE Claude's avatar
MARCHE Claude committed
149

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
150
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
151 152 153 154 155 156 157 158 159
are the following.
\begin{enumerate}
\item Completely redesigned input syntax for logic declarations
  \begin{itemize}
  \item new syntax for terms and formulas
  \item enumerated and algebraic data types, pattern matching
  \item recursive definitions of logic functions and predicates, with
    termination checking
  \item inductive definitions of predicates
160
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
161 162 163 164 165
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
166
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
167 168 169
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
170

MARCHE Claude's avatar
MARCHE Claude committed
171
\item Source code organized as a library with a documented API, to
MARCHE Claude's avatar
MARCHE Claude committed
172
  allow access to \why features programmatically.
MARCHE Claude's avatar
MARCHE Claude committed
173

174
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
175 176 177 178 179 180 181 182
  \begin{itemize}
  \item session save and restore
  \item prover calls in parallel
  \item splitting, and more generally applying task transformations,
    on demand
  \item ability to edit proofs for interactive provers (Coq only for
    the moment) on any subtask
  \end{itemize}
183

MARCHE Claude's avatar
MARCHE Claude committed
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205
\item Extensible architecture via plugins
  \begin{itemize}
  \item users can define new transformations
  \item users can add connections to additional provers
  \end{itemize}
\end{enumerate}

% \begin{itemize}
% \item New syntax for terms and formulas
% \item Algebraic data types, pattern matching
% \item Recursive definitions
% \item Inductive predicates
% \item Declaration encapsulated in theories. Using and cloning theories.
% \item Concept of proof task transformation
% \item Generic communication with provers
% \item OCaml library with documented API
% \item New GUI with session save and restore
% % \item New syntax for programs, new VC generator, intentionaly left *)
% %   undocumented, since the syntax is likely to evolve significantly in *)
% %   the future. Examples are available in \texttt{examples/programs}. *)
% \end{itemize}

MARCHE Claude's avatar
MARCHE Claude committed
206 207 208 209
\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
210

211
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
212

MARCHE Claude's avatar
MARCHE Claude committed
213 214
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
215 216
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
217
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
218

MARCHE Claude's avatar
MARCHE Claude committed
219
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
220

221
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
222

MARCHE Claude's avatar
doc  
MARCHE Claude committed
223 224
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
225 226
\part{Reference Manual}

227 228 229 230
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
231 232 233 234
\input{syntaxref.tex}

\input{library.tex}

235 236
\input{realizations.tex}

237
\input{coq_tactic.tex}
238

239 240
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
241

242
% \input{./apidoc.tex} *)
MARCHE Claude's avatar
MARCHE Claude committed
243

244 245 246 247
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
248
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
249 250
\bibliography{manual}
%\input{biblio-demons}
251

MARCHE Claude's avatar
MARCHE Claude committed
252

MARCHE Claude's avatar
MARCHE Claude committed
253 254 255
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
256 257
\cleardoublepage
\listoffigures
258 259 260
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
261
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
262 263 264 265 266 267

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