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

13 14
%HEVEA\@addimagenopt{-pdf}

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

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

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

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

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

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

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

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

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

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

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

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

% 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
77
\input{./macros.tex}
78
\input{./replayer_macros.tex}
MARCHE Claude's avatar
MARCHE Claude committed
79 80
\input{./version.tex}

81 82
\makeindex

83 84
%HEVEA\title{The Why3 platform}

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

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

\begin{center}

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

\vfill

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

\vfill

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

\vfill

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

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

\vfill

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

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
145
\begin{tabular}{l}
146 147
$^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
148 149
\end{tabular}

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

154
\textcopyright 2010--2018 University Paris-Sud, CNRS, Inria
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
155

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

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
163
  \urlutcat\end{latexonly}) ; the `\ahref{\urlhilite}{Hi-Lite}'
MARCHE Claude's avatar
MARCHE Claude committed
164
\begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
MARCHE Claude's avatar
MARCHE Claude committed
165
System@tic competitivity cluster ; the `\ahref{\urlbware}{BWare}'
MARCHE Claude's avatar
MARCHE Claude committed
166
ANR project (ANR-12-INSE-0010\begin{latexonly},
MARCHE Claude's avatar
MARCHE Claude committed
167
  \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
168 169
\end{flushleft}
\end{center}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
170

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

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

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

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

203 204 205
\why is also distributed under the form of an OPAM package and a
Debian package.

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

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
213
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
214 215 216 217

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
218
Report any bug to the \why Bug Tracking System:
219
\url{https://gitlab.inria.fr/why3/why3/issues}.
MARCHE Claude's avatar
MARCHE Claude committed
220 221


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

MARCHE Claude's avatar
MARCHE Claude committed
224
We gratefully thank the people who contributed to \why, directly or
MARCHE Claude's avatar
MARCHE Claude committed
225
indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin
226 227 228 229 230
Clochard, Simon Cruanes, Sylvain Dailler, Cl\'ement Fumex, L\'eon
Gondelman, David Hauzar, Daisuke Ishii, Johannes Kanig, St\'ephane
Lescuyer, Mikhail Mandrykin, David Mentr\'e, Sim\~ao Melo de Sousa,
Benjamin Monate, Kim Nguyen, Thi-Minh-Tuyen Nguyen, M\'ario Pereira,
Asma Tafat, Piotr Trojanek, Makarius Wenzel.
MARCHE Claude's avatar
MARCHE Claude committed
231

MARCHE Claude's avatar
MARCHE Claude committed
232

233 234 235 236 237 238 239 240 241 242 243 244
\cleardoublepage

%BEGIN LATEX
\tableofcontents
%END LATEX

%\input{intro.tex}

\part{Tutorial}

\input{starting.tex}

245
% \input{syntax.tex}
246 247 248 249 250 251 252 253 254 255 256 257 258 259 260

% \input{ide.tex}

\input{whyml.tex}

\input{api.tex}

\part{Reference Manual}

\input{install.tex}

\input{manpages.tex}

\input{syntaxref.tex}

261 262 263 264
\input{exec.tex}

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

266
\input{itp.tex}
267 268 269 270 271 272 273 274 275 276 277 278 279 280


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

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

\input{technical.tex}

\part{Appendix}

\appendix

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

MARCHE Claude's avatar
MARCHE Claude committed
283 284 285 286 287 288 289 290 291 292 293 294 295 296 297
\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}
298

299 300 301 302 303 304
Logical symbols can no longer be used in non-ghost code;
in particular, there is no polymorphic equality in programs any more,
so equality functions must be declared/defined on a per-type basis
(already done for type \texttt{int} in the standard library). The CHANGES
file contains other potential incompatibility.

305
\begin{center}
306
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
307
\hline
308
\textbf{version 0.87} & \textbf{version 0.90} \\
309
\hline
310 311 312
\texttt{function f ...} & \texttt{let function f ...} if called in
                          programs \\
\hline
313
\texttt{'L:} & \texttt{label L in} \\
314
\hline
315
\texttt{at x 'L} & \texttt{x at L} \\
316 317 318
\hline
\texttt{assert \{ ... (old x) ... \}} & \texttt{assert \{ ... (x at Init) ... \}} \\
\hline
Guillaume Melquiond's avatar
Guillaume Melquiond committed
319
\texttt{\char`\\ x. e} & \texttt{fun x -> e} \\
320
\hline
321
\texttt{use HighOrd} & nothing, not needed anymore \\
322
\hline
323
\texttt{HighOrd.pred ty} & \texttt{ty -> bool} \\
324 325 326
\hline
\texttt{type t model ...} & \texttt{type t = abstract ...} \\
\hline
327
\texttt{abstract e ensures \{ Q \}} & \texttt{begin ensures \{ Q \} e end} \\
328
\hline
329 330 331 332
\texttt{namespace N} & \texttt{scope N} \\
\hline
\texttt{"attribute"} & \texttt{[@attribute]} \\
\hline
333 334
\texttt{meta M prop P} & \texttt{meta M lemma P} or \texttt{meta M axiom P} or \texttt{meta M goal P} \\
\hline
Guillaume Melquiond's avatar
Guillaume Melquiond committed
335 336 337 338
\texttt{loop ... end} & \texttt{while true do ... done} \\
\hline
\texttt{type ... invariant \{ ... self.foo ... \}} & \texttt{type ... invariant \{ ... foo ... \}}\\
\hline
339
\end{tabular}
340 341
\end{center}

MARCHE Claude's avatar
MARCHE Claude committed
342 343 344 345 346 347 348 349 350 351 352 353 354
\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

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

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

360
\begin{figure}[thbp]
361
  \centering
362
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
363
\hline
364 365
\textbf{version 0.73} & \textbf{version 0.80} \\
\hline
366 367
\ttfamily
type t = \{| field~:~int |\}
368
&
369 370
\ttfamily
type t = \{ field~:~int \}
371 372
\\
\hline
373 374
\ttfamily
\{| field = 5 |\}
375
&
376 377
\ttfamily
\{ field = 5 \}
378
\\
379
\hline
380 381
\ttfamily
use import module M
382
&
383 384
\ttfamily
use import M
385 386
\\
\hline
387 388 389 390 391 392 393 394
\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 \}
395
&
396 397 398 399 400 401 402 403
\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
404 405
\\
\hline
406 407 408 409 410 411 412 413
\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 \}
414
&
415 416 417 418 419 420 421
\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 \}
422 423
\\
\hline
424 425 426 427 428 429 430 431
\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 \}
432
&
433 434 435 436 437 438 439
\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 \}
440 441
\\
\hline
442 443
\ttfamily
abstract e \{ Q \}
444
&
445 446
\ttfamily
abstract e ensures \{ Q \}
447 448 449 450 451 452 453
\\
\hline
\end{tabular}
\caption{Syntax changes from version 0.73 to version 0.80}
\label{fig:syntax080}
\end{figure}

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
457 458 459 460 461 462 463 464 465
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
466
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
467 468 469 470 471
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
472
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
473 474 475
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
476

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

480
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
481 482 483 484 485 486 487 488
  \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}
489

MARCHE Claude's avatar
MARCHE Claude committed
490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511
\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}

512
\bibliographystyle{plain}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
513
\bibliography{manual}
514
%\bibliography{abbrevs,demons,demons2,demons3,team,crossrefs}
515

MARCHE Claude's avatar
MARCHE Claude committed
516

MARCHE Claude's avatar
MARCHE Claude committed
517 518 519
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
520 521
\cleardoublepage
\listoffigures
522 523 524
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
525
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
526 527 528 529 530 531

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