manual.tex 12.4 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 7 8 9 10 11
%BEGIN LATEX
\usepackage{comment}
\newcommand{\ahref}[2]{{#2}}
\excludecomment{htmlonly}
\newenvironment{latexonly}{}{}
%END LATEX

12 13
%HEVEA\@addimagenopt{-pdf}

14
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
15 16
% tells memoir style to number subsections
\setsecnumdepth{subsection}
17
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
18

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
19
\usepackage[T1]{fontenc}
20
\usepackage{lmodern}
21
%\usepackage{url}
22
\usepackage[pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
MARCHE Claude's avatar
MARCHE Claude committed
23

24 25 26 27
%BEGIN LATEX
\usepackage{upquote}
%END LATEX

MARCHE Claude's avatar
MARCHE Claude committed
28
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
29
\usepackage{graphicx}
MARCHE Claude's avatar
MARCHE Claude committed
30 31 32
%END LATEX
%HEVEA \newcommand{\includegraphics}[2][2]{\imgsrc{#2}}

33
\usepackage{listings}
MARCHE Claude's avatar
MARCHE Claude committed
34
\usepackage{xspace}
MARCHE Claude's avatar
MARCHE Claude committed
35

36
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
37 38 39 40 41
\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
\setheadfoot{15pt}{38pt}
\checkandfixthelayout

MARCHE Claude's avatar
MARCHE Claude committed
42 43 44 45
% placement of figures
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}
46
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
47 48 49
\setcounter{topnumber}{4}
\setcounter{bottomnumber}{4}
\setcounter{totalnumber}{8}
MARCHE Claude's avatar
MARCHE Claude committed
50

MARCHE Claude's avatar
MARCHE Claude committed
51
%HEVEA \newstyle{table.lstframe}{width:100\%;border-width:1px;}
52

MARCHE Claude's avatar
MARCHE Claude committed
53 54 55 56 57 58
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
60
% for ocamldoc generated pages
61
%\usepackage{ocamldoc}
62 63
%\let\tt\ttfamily
%\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
64

MARCHE Claude's avatar
MARCHE Claude committed
65
\usepackage{ifthen}
66 67 68 69 70 71 72 73 74 75

% avoid double spacing after '.' and ':' in texttt
%BEGIN LATEX
\makeatletter
\let\ttfamily\relax
\DeclareRobustCommand\ttfamily
   {\not@math@alphabet\ttfamily\mathtt\fontfamily\ttdefault\selectfont\frenchspacing}
\makeatother
%END LATEX

MARCHE Claude's avatar
MARCHE Claude committed
76
\input{./macros.tex}
77
\input{./replayer_macros.tex}
MARCHE Claude's avatar
MARCHE Claude committed
78 79
\input{./version.tex}

80 81
\makeindex

82 83
%HEVEA\title{The Why3 platform}

MARCHE Claude's avatar
MARCHE Claude committed
84
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
85
\sloppy
86
%BEGIN LATEX
87
\hbadness=5000
88
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
89

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
90 91 92 93
\thispagestyle{empty}

\begin{center}

94
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
95
\rule\textwidth{0.8mm}
96
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
97 98 99

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
100 101 102 103 104 105
{
%BEGIN LATEX
\fontsize{40}{40pt}\selectfont
%END LATEX
%HEVEA \Huge
\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
106 107 108

\vfill

109
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
110
\rule\textwidth{0.8mm}
111
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
112 113 114

\vfill

115
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
116

117
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
118
\begin{LARGE}
119
%END LATEX
Guillaume Melquiond's avatar
Guillaume Melquiond committed
120
  Version \whyversion{}, January 2018
121
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
122
\end{LARGE}
123
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
124 125 126

\vfill

127
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
128
\begin{Large}
129
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
130
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
131 132 133
  Fran\c{c}ois Bobot$^{1,2}$ \\
  Jean-Christophe Filli\^atre$^{1,2}$  \\
  Claude March\'e$^{2,1}$ \\
134
  Guillaume Melquiond$^{2,1}$\\
MARCHE Claude's avatar
MARCHE Claude committed
135
  Andrei Paskevich$^{1,2}$
MARCHE Claude's avatar
MARCHE Claude committed
136
\end{tabular}
137
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
138
\end{Large}
139
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
140 141 142 143
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
144
\begin{tabular}{l}
145 146
$^1$ LRI, CNRS \& University Paris-Sud, Orsay, F-91405 \\
$^2$ Inria Saclay -- \^Ile-de-France, Palaiseau, F-91120
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
147 148
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
149
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
150
\bigskip
MARCHE Claude's avatar
MARCHE Claude committed
151
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
152

Andrei Paskevich's avatar
Andrei Paskevich committed
153
\textcopyright 2010--2016 University Paris-Sud, CNRS, Inria
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
154

155
\urldef{\urlutcat}{\url}{http://frama-c.com/u3cat/}
156
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
MARCHE Claude's avatar
MARCHE Claude committed
157
\urldef{\urlbware}{\url}{http://bware.lri.fr/}
MARCHE Claude's avatar
MARCHE Claude committed
158
\urldef{\urlproofinuse}{\url}{http://www.spark-2014.org/proofinuse}
MARCHE Claude's avatar
MARCHE Claude committed
159 160 161

This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
MARCHE Claude's avatar
MARCHE Claude committed
162
  \urlutcat\end{latexonly}) ; the `\ahref{\urlhilite}{Hi-Lite}'
MARCHE Claude's avatar
MARCHE Claude committed
163
\begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
MARCHE Claude's avatar
MARCHE Claude committed
164
System@tic competitivity cluster ; the `\ahref{\urlbware}{BWare}'
MARCHE Claude's avatar
MARCHE Claude committed
165
ANR project (ANR-12-INSE-0010\begin{latexonly},
MARCHE Claude's avatar
MARCHE Claude committed
166
  \urlbware\end{latexonly}) ; and the \ahref{\urlproofinuse}{Joint Laboratory ProofInUse} (ANR-13-LAB3-0007\begin{latexonly}, \urlproofinuse\end{latexonly})
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
167 168
\end{flushleft}
\end{center}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
169

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
170
\chapter*{Foreword}
171
%HEVEA\cutname{foreword.html}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
172

173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189
%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
190 191 192 193 194
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
195

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
196
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
197

MARCHE Claude's avatar
MARCHE Claude committed
198 199 200
\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
201

MARCHE Claude's avatar
MARCHE Claude committed
202
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
203 204 205
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
206
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
207 208
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
209
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
210 211 212 213

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


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

MARCHE Claude's avatar
MARCHE Claude committed
220
We gratefully thank the people who contributed to \why, directly or
MARCHE Claude's avatar
MARCHE Claude committed
221
indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin
Leon Gondelman's avatar
Leon Gondelman committed
222
Clochard, Simon Cruanes, L\'eon Gondelman, Johannes Kanig, St\'ephane
MARCHE Claude's avatar
MARCHE Claude committed
223
Lescuyer, David Mentr\'e, Sim\~ao Melo de Sousa, Benjamin Monate,
Leon Gondelman's avatar
Leon Gondelman committed
224
Thi-Minh-Tuyen Nguyen, M\'ario Pereira, Asma Tafat, Piotr Trojanek.
MARCHE Claude's avatar
MARCHE Claude committed
225

MARCHE Claude's avatar
MARCHE Claude committed
226

227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
\cleardoublepage

%BEGIN LATEX
\tableofcontents
%END LATEX

%\input{intro.tex}

\part{Tutorial}

\input{starting.tex}

\input{syntax.tex}

% \input{ide.tex}

\input{whyml.tex}

\input{api.tex}

\part{Reference Manual}

\input{install.tex}

\input{manpages.tex}

\input{syntaxref.tex}

255 256 257 258
\input{exec.tex}

% maintaining library.tex up to date is hopeless
% \input{library.tex}
259

260
\input{itp.tex}
261 262 263 264 265 266 267 268 269 270 271 272 273 274


% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)

% \input{./apidoc.tex} *)

\input{technical.tex}

\part{Appendix}

\appendix

\chapter{Release Notes}
275
%HEVEA\cutname{changes.html}
MARCHE Claude's avatar
MARCHE Claude committed
276

MARCHE Claude's avatar
MARCHE Claude committed
277 278 279 280 281 282 283 284 285 286 287 288 289 290 291
\section{Release Notes for version 0.90}

TO DISCUSS:

comment mettre a jour l'example bag ? Parametrer par une egalit'e sur
les elements ?


Attention, ne pas introduire 1 variable par champ complique le boulot des prouveurs

``inline'' ne doit pas inliner Map.set

egalite sur les type algebriques ? engendrees automatiquement ?

\subsection{Syntax Changes}
292 293

\begin{center}
294
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
295
\hline
296
\textbf{version 0.87} & \textbf{version 0.90} \\
297 298
\hline
\texttt{'L:} & \texttt{label L in} \\
299
\hline
300
\texttt{at x 'L} & \texttt{x at L} \\
301 302 303 304 305
\hline
\texttt{assert \{ ... (old x) ... \}} & \texttt{assert \{ ... (x at Init) ... \}} \\
\hline
\texttt{\char`\\ x{.} e} & \texttt{fun x -> e} \\
\hline
306
\texttt{use HighOrd} & nothing, not needed anymore \\
307
\hline
308
\texttt{HighOrd.pred ty} & \texttt{ty -> bool} \\
309 310 311
\hline
\texttt{type t model ...} & \texttt{type t = abstract ...} \\
\hline
312
\texttt{abstract e ensures \{ Q \}} & \texttt{begin ensures \{ Q \} e end} \\
313
\hline
314 315 316 317 318
\texttt{namespace N} & \texttt{scope N} \\
\hline
\texttt{"attribute"} & \texttt{[@attribute]} \\
\hline
\end{tabular}
319 320
\end{center}

MARCHE Claude's avatar
MARCHE Claude committed
321 322 323 324 325 326 327 328 329 330 331 332 333
\subsection{Model types, abstract types}

explain \texttt{private} and ghost fields, \texttt{abstract mutable},
\texttt{private mutable}

\subsection{Polymorphic Equality}

No polymorphic equality in programs. Consequence : no List.mem in
programs, need for List.mem, List.filter, parameterized with a
predicate.

No default equality on algebraic datatypes

334
\section{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
335

MARCHE Claude's avatar
MARCHE Claude committed
336
The syntax of \whyml programs changed in release 0.80.
337
The table in Figure~\ref{fig:syntax080} summarizes the changes.
338

339
\begin{figure}[thbp]
340
  \centering
341
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
342
\hline
343 344
\textbf{version 0.73} & \textbf{version 0.80} \\
\hline
345 346
\ttfamily
type t = \{| field~:~int |\}
347
&
348 349
\ttfamily
type t = \{ field~:~int \}
350 351
\\
\hline
352 353
\ttfamily
\{| field = 5 |\}
354
&
355 356
\ttfamily
\{ field = 5 \}
357
\\
358
\hline
359 360
\ttfamily
use import module M
361
&
362 363
\ttfamily
use import M
364 365
\\
\hline
366 367 368 369 370 371 372 373
\ttfamily
let rec f (x:int) (y:int)~:~t \newline
\null~~~~variant \{ t \} with rel = \newline
\null~~~~\{ P \} \newline
\null~~~~e \newline
\null~~~~\{ Q \} \newline
\null~~~~| Exc1 -> \{ R1 \} \newline
\null~~~~| Exc2 n -> \{ R2 \}
374
&
375 376 377 378 379 380 381 382
\ttfamily
let rec f (x:int) (y:int)~:~t \newline
\null~~~~variant \{ t with rel \} \newline
\null~~~~requires \{ P \} \newline
\null~~~~ensures \{ Q \} \newline
\null~~~~raises \{ Exc1 -> R1 \newline
\null~~~~~~~~~~~| Exc2 n -> R2 \} \newline
\null~~~~= e
383 384
\\
\hline
385 386 387 388 389 390 391 392
\ttfamily
val f (x:int) (y:int)~:\newline
\null~~~~\{ P \} \newline
\null~~~~t \newline
\null~~~~writes a b \newline
\null~~~~\{ Q \} \newline
\null~~~~| Exc1 -> \{ R1 \} \newline
\null~~~~| Exc2 n -> \{ R2 \}
393
&
394 395 396 397 398 399 400
\ttfamily
val f (x:int) (y:int)~:~t \newline
\null~~~~requires \{ P \} \newline
\null~~~~writes \{ a, b \} \newline
\null~~~~ensures \{ Q \} \newline
\null~~~~raises \{ Exc1 -> R1 \newline
\null~~~~~~~~~~~| Exc2 n -> R2 \}
401 402
\\
\hline
403 404 405 406 407 408 409 410
\ttfamily
val f~:~x:int -> y:int ->\newline
\null~~~~\{ P \} \newline
\null~~~~t \newline
\null~~~~writes a b \newline
\null~~~~\{ Q \} \newline
\null~~~~| Exc1 -> \{ R1 \} \newline
\null~~~~| Exc2 n -> \{ R2 \}
411
&
412 413 414 415 416 417 418
\ttfamily
val f (x y:int)~:~t \newline
\null~~~~requires \{ P \} \newline
\null~~~~writes \{ a, b \} \newline
\null~~~~ensures \{ Q \} \newline
\null~~~~raises \{ Exc1 -> R1 \newline
\null~~~~~~~~~~~| Exc2 n -> R2 \}
419 420
\\
\hline
421 422
\ttfamily
abstract e \{ Q \}
423
&
424 425
\ttfamily
abstract e ensures \{ Q \}
426 427 428 429 430 431 432
\\
\hline
\end{tabular}
\caption{Syntax changes from version 0.73 to version 0.80}
\label{fig:syntax080}
\end{figure}

433
\section{Summary of Changes w.r.t. Why 2}
MARCHE Claude's avatar
MARCHE Claude committed
434

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
435
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
436 437 438 439 440 441 442 443 444
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
445
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
446 447 448 449 450
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
451
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
452 453 454
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
455

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

459
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
460 461 462 463 464 465 466 467
  \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}
468

MARCHE Claude's avatar
MARCHE Claude committed
469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490
\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}

491
\bibliographystyle{abbrvurl}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
492
\bibliography{manual}
493
%\bibliography{abbrevs,demons,demons2,demons3,team,crossrefs}
494

MARCHE Claude's avatar
MARCHE Claude committed
495

MARCHE Claude's avatar
MARCHE Claude committed
496 497 498
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
499 500
\cleardoublepage
\listoffigures
501 502 503
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
504
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
505 506 507 508 509 510

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