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

3 4
% rubber: module index

5 6
%HEVEA\@addimagenopt{-pdf}

7
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
8 9
% tells memoir style to number subsections
\setsecnumdepth{subsection}
10
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
11

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
12
\usepackage[T1]{fontenc}
13
\usepackage{lmodern}
14
%\usepackage{url}
15
\usepackage[pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
MARCHE Claude's avatar
MARCHE Claude committed
16 17

%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
18
\usepackage{graphicx}
MARCHE Claude's avatar
MARCHE Claude committed
19 20 21
%END LATEX
%HEVEA \newcommand{\includegraphics}[2][2]{\imgsrc{#2}}

22
\usepackage{listings}
MARCHE Claude's avatar
MARCHE Claude committed
23
\usepackage{xspace}
24
\usepackage{hevea}
MARCHE Claude's avatar
MARCHE Claude committed
25

26
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30 31
\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
\setheadfoot{15pt}{38pt}
\checkandfixthelayout

MARCHE Claude's avatar
MARCHE Claude committed
32 33 34 35
% placement of figures
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}
36
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
37 38 39
\setcounter{topnumber}{4}
\setcounter{bottomnumber}{4}
\setcounter{totalnumber}{8}
MARCHE Claude's avatar
MARCHE Claude committed
40

MARCHE Claude's avatar
MARCHE Claude committed
41 42 43 44 45 46
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
48
% for ocamldoc generated pages
49
%\usepackage{ocamldoc}
50 51
%\let\tt\ttfamily
%\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
52

MARCHE Claude's avatar
MARCHE Claude committed
53 54
\usepackage{ifthen}
\input{./macros.tex}
55
\input{./replayer_macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
56

MARCHE Claude's avatar
MARCHE Claude committed
57 58
\input{./version.tex}

59 60
\makeindex

61 62
%HEVEA\title{The Why3 platform}

MARCHE Claude's avatar
MARCHE Claude committed
63
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
64
\sloppy
65
%BEGIN LATEX
66
\hbadness=5000
67
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
68

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
69 70 71 72
\thispagestyle{empty}

\begin{center}

73
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
74
\rule\textwidth{0.8mm}
75
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
76 77 78

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
79 80 81 82 83 84
{
%BEGIN LATEX
\fontsize{40}{40pt}\selectfont
%END LATEX
%HEVEA \Huge
\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
85 86 87

\vfill

88
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
89
\rule\textwidth{0.8mm}
90
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
91 92 93

\vfill

94
\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
95

96
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
97
\begin{LARGE}
98
%END LATEX
99
  Version \whyversion{}, October 2012
100
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
101
\end{LARGE}
102
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
103 104 105

\vfill

106
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
107
\begin{Large}
108
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
109
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
110 111 112
  Fran\c{c}ois Bobot$^{1,2}$ \\
  Jean-Christophe Filli\^atre$^{1,2}$  \\
  Claude March\'e$^{2,1}$ \\
113
  Guillaume Melquiond$^{2,1}$\\
MARCHE Claude's avatar
MARCHE Claude committed
114
  Andrei Paskevich$^{1,2}$
MARCHE Claude's avatar
MARCHE Claude committed
115
\end{tabular}
116
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
117
\end{Large}
118
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
119 120 121 122
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
123
\begin{tabular}{l}
MARCHE Claude's avatar
MARCHE Claude committed
124
$^1$ LRI, CNRS, Univ Paris-Sud, Orsay, F-91405 \\
Guillaume Melquiond's avatar
Guillaume Melquiond committed
125
$^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
126 127
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
128
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
129
\bigskip
MARCHE Claude's avatar
MARCHE Claude committed
130
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
131

132
  \textcopyright 2010-2012 Univ Paris-Sud, CNRS, Inria
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
133

134 135 136
\urldef{\urlutcat}{\url}{http://frama-c.cea.fr/u3cat}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}

137 138 139 140 141
  This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
  national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
  \urlutcat\end{latexonly}) and by the `\ahref{\urlhilite}{Hi-Lite}'
  \begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
  System@tic competitivity cluster.
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
142 143 144

\end{flushleft}
\end{center}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
145

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
146 147
\chapter*{Foreword}

148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164
%This is the manual for the Why platform version 3, or \why for
%short.
\why is a platform for deductive program verification. It provides
a rich language for specification and programming, called \whyml, and
relies on external theorem provers, both automated and interactive,
to discharge verification conditions. \why comes with a standard
library of logical theories (integer and real arithmetic, Boolean
operations, sets and maps, etc.) and basic programming data structures
(arrays, queues, hash tables, etc.). A user can write \whyml programs
directly and get correct-by-construction OCaml programs through an
automated extraction mechanism. \whyml is also used as an intermediate
language for the verification of C, Java, or Ada programs.

\why is a complete reimplementation %~\cite{boogie11why3}
of the former Why platform~\cite{filliatre07cav}.
%for program verification.
Among the new features are: numerous
165 166 167 168 169
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
170

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
171
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
172

MARCHE Claude's avatar
MARCHE Claude committed
173 174 175
\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
176

MARCHE Claude's avatar
MARCHE Claude committed
177
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
178 179 180
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
181
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
182 183
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
184
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
185 186 187 188

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
189
Report any bug to the \why Bug Tracking System:
MARCHE Claude's avatar
MARCHE Claude committed
190 191 192
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.


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

MARCHE Claude's avatar
MARCHE Claude committed
195
We gratefully thank the people who contributed to \why, directly or
196 197
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
198

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
201
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
202 203 204 205 206 207 208 209 210
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
211
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
212 213 214 215 216
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
217
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
218 219 220
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
221

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

225
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
226 227 228 229 230 231 232 233
  \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}
234

MARCHE Claude's avatar
MARCHE Claude committed
235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256
\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
257 258
\cleardoublepage

MARCHE Claude's avatar
MARCHE Claude committed
259
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
260
\tableofcontents
MARCHE Claude's avatar
MARCHE Claude committed
261
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
262

263
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
264

MARCHE Claude's avatar
MARCHE Claude committed
265 266
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
267 268
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
269
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
270

MARCHE Claude's avatar
MARCHE Claude committed
271
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
272

273
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
274

MARCHE Claude's avatar
doc  
MARCHE Claude committed
275 276
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
277 278
\part{Reference Manual}

279 280 281 282
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
283 284 285 286
\input{syntaxref.tex}

\input{library.tex}

287 288
\input{realizations.tex}

289
\input{coq_tactic.tex}
290

291 292
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
293

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

296 297 298 299
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
300
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
301 302
\bibliography{manual}
%\input{biblio-demons}
303

MARCHE Claude's avatar
MARCHE Claude committed
304

MARCHE Claude's avatar
MARCHE Claude committed
305 306 307
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
308 309
\cleardoublepage
\listoffigures
310 311 312
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
313
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
314 315 316 317 318 319

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