manual.tex 11.9 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 66
\usepackage{ifthen}
\input{./macros.tex}
67
\input{./replayer_macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
68

MARCHE Claude's avatar
MARCHE Claude committed
69 70
\input{./version.tex}

71 72
\makeindex

73 74
%HEVEA\title{The Why3 platform}

MARCHE Claude's avatar
MARCHE Claude committed
75
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
76
\sloppy
77
%BEGIN LATEX
78
\hbadness=5000
79
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
80

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
81 82 83 84
\thispagestyle{empty}

\begin{center}

85
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
86
\rule\textwidth{0.8mm}
87
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
88 89 90

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
91 92 93 94 95 96
{
%BEGIN LATEX
\fontsize{40}{40pt}\selectfont
%END LATEX
%HEVEA \Huge
\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
97 98 99

\vfill

100
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
101
\rule\textwidth{0.8mm}
102
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
103 104 105

\vfill

106
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
107

108
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
109
\begin{LARGE}
110
%END LATEX
Guillaume Melquiond's avatar
Guillaume Melquiond committed
111
  Version \whyversion{}, January 2017
112
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
113
\end{LARGE}
114
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
115 116 117

\vfill

118
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
119
\begin{Large}
120
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
121
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
122 123 124
  Fran\c{c}ois Bobot$^{1,2}$ \\
  Jean-Christophe Filli\^atre$^{1,2}$  \\
  Claude March\'e$^{2,1}$ \\
125
  Guillaume Melquiond$^{2,1}$\\
MARCHE Claude's avatar
MARCHE Claude committed
126
  Andrei Paskevich$^{1,2}$
MARCHE Claude's avatar
MARCHE Claude committed
127
\end{tabular}
128
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
129
\end{Large}
130
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
131 132 133 134
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
135
\begin{tabular}{l}
136 137
$^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
138 139
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
140
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
141
\bigskip
MARCHE Claude's avatar
MARCHE Claude committed
142
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
143

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

146
\urldef{\urlutcat}{\url}{http://frama-c.com/u3cat/}
147
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
MARCHE Claude's avatar
MARCHE Claude committed
148
\urldef{\urlbware}{\url}{http://bware.lri.fr/}
MARCHE Claude's avatar
MARCHE Claude committed
149
\urldef{\urlproofinuse}{\url}{http://www.spark-2014.org/proofinuse}
MARCHE Claude's avatar
MARCHE Claude committed
150 151 152

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
153
  \urlutcat\end{latexonly}) ; the `\ahref{\urlhilite}{Hi-Lite}'
MARCHE Claude's avatar
MARCHE Claude committed
154
\begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
MARCHE Claude's avatar
MARCHE Claude committed
155
System@tic competitivity cluster ; the `\ahref{\urlbware}{BWare}'
MARCHE Claude's avatar
MARCHE Claude committed
156
ANR project (ANR-12-INSE-0010\begin{latexonly},
MARCHE Claude's avatar
MARCHE Claude committed
157
  \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
158 159
\end{flushleft}
\end{center}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
160

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
161
\chapter*{Foreword}
162
%HEVEA\cutname{foreword.html}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
163

164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180
%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
181 182 183 184 185
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
186

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
187
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
188

MARCHE Claude's avatar
MARCHE Claude committed
189 190 191
\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
192

MARCHE Claude's avatar
MARCHE Claude committed
193
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
194 195 196
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
197
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
198 199
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
200
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
201 202 203 204

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


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

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

MARCHE Claude's avatar
MARCHE Claude committed
217

218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
\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}

246 247 248 249
\input{exec.tex}

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

251
\input{itp.tex}
252 253 254 255 256 257 258 259 260 261 262 263 264 265


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

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

\input{technical.tex}

\part{Appendix}

\appendix

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

MARCHE Claude's avatar
MARCHE Claude committed
268 269 270 271 272 273 274 275 276 277 278 279 280 281 282
\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}
283 284 285 286 287 288 289

\begin{center}
  \begin{tabular}{|c|c|}
\hline
    0.87 & 0.90 \\
\hline
\texttt{'L:} & \texttt{label L in} \\
290 291
\texttt{at x 'L} & \texttt{x at L} \\
\texttt{assert \{ ... (old x) ... \}} & \texttt{ assert \{... (x at Init) .. \}} \\
MARCHE Claude's avatar
MARCHE Claude committed
292
\verb|\|\texttt{ x. e} & \texttt{fun x -> e} \\
293 294
\texttt{use HighOrd} & nothing, not needed anymore \\
\texttt{HighOrd.pred ty} & \texttt{ty -> bool} \\
MARCHE Claude's avatar
MARCHE Claude committed
295
\texttt{type t model ...} & \texttt{type t = abstract ... } \\
296
\texttt{abstract e ensures \{ Q \}} & \texttt{begin ensures \{ Q \} e end} \\
297 298 299 300
\hline
  \end{tabular}
\end{center}

MARCHE Claude's avatar
MARCHE Claude committed
301 302 303 304 305 306 307 308 309 310 311 312 313
\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

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

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

319
\begin{figure}[thbp]
320
  \centering
321
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
322
\hline
323 324
\textbf{version 0.73} & \textbf{version 0.80} \\
\hline
325 326
\ttfamily
type t = \{| field~:~int |\}
327
&
328 329
\ttfamily
type t = \{ field~:~int \}
330 331
\\
\hline
332 333
\ttfamily
\{| field = 5 |\}
334
&
335 336
\ttfamily
\{ field = 5 \}
337
\\
338
\hline
339 340
\ttfamily
use import module M
341
&
342 343
\ttfamily
use import M
344 345
\\
\hline
346 347 348 349 350 351 352 353
\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 \}
354
&
355 356 357 358 359 360 361 362
\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
363 364
\\
\hline
365 366 367 368 369 370 371 372
\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 \}
373
&
374 375 376 377 378 379 380
\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 \}
381 382
\\
\hline
383 384 385 386 387 388 389 390
\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 \}
391
&
392 393 394 395 396 397 398
\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 \}
399 400
\\
\hline
401 402
\ttfamily
abstract e \{ Q \}
403
&
404 405
\ttfamily
abstract e ensures \{ Q \}
406 407 408 409 410 411 412
\\
\hline
\end{tabular}
\caption{Syntax changes from version 0.73 to version 0.80}
\label{fig:syntax080}
\end{figure}

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
415
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
416 417 418 419 420 421 422 423 424
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
425
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
426 427 428 429 430
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
431
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
432 433 434
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
435

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

439
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
440 441 442 443 444 445 446 447
  \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}
448

MARCHE Claude's avatar
MARCHE Claude committed
449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470
\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
471
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
472 473
\bibliography{manual}
%\input{biblio-demons}
474

MARCHE Claude's avatar
MARCHE Claude committed
475

MARCHE Claude's avatar
MARCHE Claude committed
476 477 478
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
479 480
\cleardoublepage
\listoffigures
481 482 483
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
484
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
485 486 487 488 489 490

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