manual.tex 18.7 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}
MARCHE Claude's avatar
MARCHE Claude committed
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

MARCHE Claude's avatar
MARCHE Claude committed
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
Guillaume Melquiond's avatar
Guillaume Melquiond committed
121
  Version \whyversion{}, January 2019
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
\urldef{\urlcolis}{\url}{http://colis.irif.univ-paris-diderot.fr/}
\urldef{\urlvocal}{\url}{https://vocal.lri.fr/}
MARCHE Claude's avatar
MARCHE Claude committed
162 163 164

This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
Guillaume Melquiond's avatar
Guillaume Melquiond committed
165
  \urlutcat\end{latexonly}), the `\ahref{\urlhilite}{Hi-Lite}'
MARCHE Claude's avatar
MARCHE Claude committed
166
\begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
Guillaume Melquiond's avatar
Guillaume Melquiond committed
167
System@tic competitivity cluster, the `\ahref{\urlbware}{BWare}'
MARCHE Claude's avatar
MARCHE Claude committed
168
ANR project (ANR-12-INSE-0010\begin{latexonly},
Guillaume Melquiond's avatar
Guillaume Melquiond committed
169
  \urlbware\end{latexonly}), the \ahref{\urlproofinuse}{Joint Laboratory ProofInUse} (ANR-13-LAB3-0007\begin{latexonly}, \urlproofinuse\end{latexonly});
MARCHE Claude's avatar
MARCHE Claude committed
170
the `\ahref{\urlcolis}{CoLiS}' ANR project (ANR-15-CE25-0001\begin{latexonly},
Guillaume Melquiond's avatar
Guillaume Melquiond committed
171 172
  \urlcolis\end{latexonly}), and the `\ahref{\urlvocal}{VOCaL}' ANR project (ANR-15-CE25-008\begin{latexonly},
  \urlvocal\end{latexonly}).
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
173 174
\end{flushleft}
\end{center}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
175

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
176
\chapter*{Foreword}
177
%HEVEA\cutname{foreword.html}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
178

179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
%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
196 197 198 199 200
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
201

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
202
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
203

MARCHE Claude's avatar
MARCHE Claude committed
204 205 206
\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
207

208 209 210
\why is also distributed under the form of an OPAM package and a
Debian package.

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

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
218
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
219 220 221 222

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


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

MARCHE Claude's avatar
MARCHE Claude committed
229
We gratefully thank the people who contributed to \why, directly or
Guillaume Melquiond's avatar
Guillaume Melquiond committed
230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251
indirectly:
Stefan Berghofer,
Sylvie Boldo,
Martin Clochard,
Simon Cruanes,
Sylvain Dailler,
Cl\'ement Fumex,
L\'eon Gondelman,
David Hauzar,
Daisuke Ishii,
Johannes Kanig,
Mikhail Mandrykin,
David Mentr\'e,
Benjamin Monate,
Kim Nguyen,
Thi-Minh-Tuyen Nguyen,
M\'ario Pereira,
Rapha\"el Rieu-Helft,
Sim\=ao Melo de Sousa,
Asma Tafat,
Piotr Trojanek,
Makarius Wenzel.
MARCHE Claude's avatar
MARCHE Claude committed
252

253 254 255 256 257 258 259 260 261 262 263 264
\cleardoublepage

%BEGIN LATEX
\tableofcontents
%END LATEX

%\input{intro.tex}

\part{Tutorial}

\input{starting.tex}

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

% \input{ide.tex}

\input{whyml.tex}

\input{api.tex}

\part{Reference Manual}

\input{install.tex}

\input{manpages.tex}

\input{syntaxref.tex}

281 282 283 284
\input{exec.tex}

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

286
\input{itp.tex}
287 288 289 290 291 292 293 294 295 296 297 298 299 300


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

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

\input{technical.tex}

\part{Appendix}

\appendix

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

303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411
\section{Release Note for version 1.2: new syntax for ``auto-dereference''}

Version 1.2 introduces a simplified syntax for reference variables, to
avoid the somehow heavy OCaml syntax using bang character. In short,
this is syntactic sugar summarized in the following table.  An example
using this new syntax is in \url{examples/isqrt.mlw}

\begin{center}
  \begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
\hline
\textbf{auto-dereference syntax} & \textbf{desugared to} \\
\hline
\texttt{let \&x = ... in} & \texttt{let (x: ref ...) = ... in} \\
\hline
\texttt{f x;} & \texttt{f x.contents;} \\
\hline
\texttt{x <- ...} & \texttt{x.contents <- ...} \\
\hline
\texttt{let ref x = ...} & \texttt{let \&x = ref ...} \\
\hline
\end{tabular}
\end{center}
Notice that:
\begin{itemize}
\item The \verb|&| marker adds the typing constraint \verb|(x: ref ...)|
\item Top-level \verb|let/val ref| and \verb|let/val &| are allowed
\item Auto-dereferencing works in logic, but such variables
  cannot be introduced inside logical terms.
\end{itemize}

That syntactic sugar is further extended to pattern matching, function
parameters and reference passing as follows.
\begin{center}
  \begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
\hline
\textbf{auto-dereference syntax} & \textbf{desugared to} \\
\hline
\texttt{match e with (x,\&y) -> y end} & \texttt{match e with
 (x,(y: ref ...)) -> y.contents end} \\
  \hline
  \texttt{\begin{tabular}{l}
            let incr (\&x: ref int) = \\
            ~ x <- x + 1 \\
            ~ \\
            let f () = \\
            ~ let ref x = 0 in \\
            ~ incr x; \\
            ~ x
          \end{tabular}}
  &
    \texttt{\begin{tabular}{l}
              let incr (x: ref int) = \\
              ~ x.contents <- x.contents + 1 \\
              ~ \\
              let f () = \\
              ~ let x = ref 0 in \\
              ~ incr x; \\
              ~ x.contents
            \end{tabular}}
  \\
  \hline
  \texttt{let incr (ref x: int)  ...} & \texttt{let incr (\&x: ref int) ...}
                                        \\\hline
\end{tabular}
\end{center}

The type annotation is not required. Let-functions with such formal
parameters also prevent the actual argument from auto-dereferencing
when used in logic. Pure logical symbols cannot be declared with such
parameters.

Auto-dereference suppression does not work in the middle of a relation
chain: in \verb|0 < x :< 17|, \verb|x| will be dereferenced even if \verb|(:<)| expects a
ref-parameter on the left.

Finally, that syntactic sugar applies to the caller side:
\begin{center}
  \begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
\hline
\textbf{auto-dereference syntax} & \textbf{desugared to} \\
\hline
 \texttt{\begin{tabular}{l}
    let f () = \\
    ~ let ref x = 0 in \\
    ~ g \&x
         \end{tabular}}
  &
 \texttt{\begin{tabular}{l}
          let f () = \\
          ~ let x = ref 0 in \\
          ~ g x
         \end{tabular}
  }
  \\\hline
\end{tabular}
\end{center}
The \verb|&| marker can only be attached to a variable. Works in logic.

Ref-binders and \verb|&|-binders in variable declarations, patterns,
and function parameters do not require importing \verb|ref.Ref|.
Any example that does not use references inside data structures
can be rewritten by using ref-binders, without importing \verb|ref.Ref|.

Explicit use of type symbol "ref", program function "ref",
or field "contents" require importing \verb|ref.Ref| or \verb|why3.Ref.Ref|.
Operations \verb|(:=)| and \verb|(!)| require importing \verb|ref.Ref|.

Operation \verb|(:=)| is fully subsumed by direct assignment \verb|(<-)|.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
412
\section{Release Notes for version 1.0: syntax changes w.r.t. 0.88}
MARCHE Claude's avatar
MARCHE Claude committed
413

Guillaume Melquiond's avatar
Guillaume Melquiond committed
414 415
The syntax of \whyml programs changed in release 1.0.
The table in Figure~\ref{fig:syntax-1.0} summarizes the changes.
MARCHE Claude's avatar
MARCHE Claude committed
416

Guillaume Melquiond's avatar
Guillaume Melquiond committed
417 418
Note also that logical symbols can no longer be used in non-ghost code;
in particular, there is no polymorphic equality in programs anymore,
419
so equality functions must be declared/defined on a per-type basis
Guillaume Melquiond's avatar
Guillaume Melquiond committed
420 421
(already done for type \texttt{int} in the standard library). The \texttt{CHANGES.md}
file describes other potential sources of incompatibility.
422

Guillaume Melquiond's avatar
Guillaume Melquiond committed
423 424
\begin{figure}[thbp]
\centering
425
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
426
\hline
Guillaume Melquiond's avatar
Guillaume Melquiond committed
427
\textbf{version 0.88} & \textbf{version 1.0} \\
428
\hline
429 430 431
\texttt{function f ...} & \texttt{let function f ...} if called in
                          programs \\
\hline
432
\texttt{'L:} & \texttt{label L in} \\
433
\hline
434
\texttt{at x 'L} & \texttt{x at L} \\
435
\hline
Guillaume Melquiond's avatar
Guillaume Melquiond committed
436
\texttt{\char`\\ x. e} & \texttt{fun x -> e} \\
437
\hline
438
\texttt{use HighOrd} & nothing, not needed anymore \\
439
\hline
440
\texttt{HighOrd.pred ty} & \texttt{ty -> bool} \\
441 442 443
\hline
\texttt{type t model ...} & \texttt{type t = abstract ...} \\
\hline
444
\texttt{abstract e ensures \{ Q \}} & \texttt{begin ensures \{ Q \} e end} \\
445
\hline
446 447
\texttt{namespace N} & \texttt{scope N} \\
\hline
448 449
\texttt{use import M} & \texttt{use M} \\
\hline
450 451
\texttt{"attribute"} & \texttt{[@attribute]} \\
\hline
452 453
\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
454 455 456 457
\texttt{loop ... end} & \texttt{while true do ... done} \\
\hline
\texttt{type ... invariant \{ ... self.foo ... \}} & \texttt{type ... invariant \{ ... foo ... \}}\\
\hline
458
\end{tabular}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
459 460 461
\caption{Syntax changes from version 0.88 to version 1.0}
\label{fig:syntax-1.0}
\end{figure}
MARCHE Claude's avatar
MARCHE Claude committed
462

463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496
Here are a few more semantic changes
\begin{description}
\item[Proving only partial correctness] In versions 0.xx of Why3, when
  a program function is recursive but not given a variant, or contains
  a while loop not given a variant, then it was assumed that the user
  wants to prove partial correctness only. A warning was issued,
  recommending to add an extra \verb|diverges| clause to that
  function's contract. It was also possible to disable that warning by
  adding the label \verb|"W:diverges:N"| to the function's
  name. Version 1.00 of Why3 is more aggressively requiring the user
  to prove the termination of functions which are not given the
  \verb|diverges| clause, and the previous warning is now an
  error. The possibility of proving only partial correctness is now
  given on a more fine-grain basis: any expression for which one wants
  to prove partial correctness only, must by annotated with the
  attribute \verb|[@vc:divergent]|.

  In other words, if one was using the following structure in Why3 0.xx:
  \begin{lstlisting}
    let f "W:diverges:N" <parameters> <contract> = <body>
  \end{lstlisting}
  then in 1.00 it should be written as
  \begin{lstlisting}
    let f <parameters> <contract> = [@vc:divergent] <body>
  \end{lstlisting}
\item[Semantics of the \texttt{any} construct] The \verb|any| construct
  in Why3 0.xx was introducing an arbitrary value satisfying the
  associated post-condition. In some sense, this construct was
  introducing some form of an axiom stating that such a value
  exists. In Why3 1.00, it is now mandatory to prove the existence of
  such a value, and a VC is generated for that purpose.

  To obtain the effect of the former semantics of the \verb|any| construct, one should use instead a local \verb|val| function. In other words, if one was using the following structure in Why3 0.xx:
  \begin{lstlisting}
MARCHE Claude's avatar
MARCHE Claude committed
497
    any t ensures { P }
498 499 500
  \end{lstlisting}
  then in 1.00 it should be written as
  \begin{lstlisting}
MARCHE Claude's avatar
MARCHE Claude committed
501
    val x:t ensures { P } in x
502 503 504 505
  \end{lstlisting}


\end{description}
506
\section{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
507

MARCHE Claude's avatar
MARCHE Claude committed
508
The syntax of \whyml programs changed in release 0.80.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
509
The table in Figure~\ref{fig:syntax-0.80} summarizes the changes.
510

511
\begin{figure}[thbp]
512
  \centering
513
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
514
\hline
515 516
\textbf{version 0.73} & \textbf{version 0.80} \\
\hline
517 518
\ttfamily
type t = \{| field~:~int |\}
519
&
520 521
\ttfamily
type t = \{ field~:~int \}
522 523
\\
\hline
524 525
\ttfamily
\{| field = 5 |\}
526
&
527 528
\ttfamily
\{ field = 5 \}
529
\\
530
\hline
531 532
\ttfamily
use import module M
533
&
534 535
\ttfamily
use import M
536 537
\\
\hline
538 539 540 541 542 543 544 545
\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 \}
546
&
547 548 549 550 551 552 553 554
\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
555 556
\\
\hline
557 558 559 560 561 562 563 564
\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 \}
565
&
566 567 568 569 570 571 572
\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 \}
573 574
\\
\hline
575 576 577 578 579 580 581 582
\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 \}
583
&
584 585 586 587 588 589 590
\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 \}
591 592
\\
\hline
593 594
\ttfamily
abstract e \{ Q \}
595
&
596 597
\ttfamily
abstract e ensures \{ Q \}
598 599 600 601
\\
\hline
\end{tabular}
\caption{Syntax changes from version 0.73 to version 0.80}
Guillaume Melquiond's avatar
Guillaume Melquiond committed
602
\label{fig:syntax-0.80}
603 604
\end{figure}

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
607
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
608 609 610 611 612 613 614 615 616
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
617
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
618 619 620 621 622
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
623
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
624 625 626
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
627

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

631
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
632 633 634 635 636 637 638 639
  \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}
640

MARCHE Claude's avatar
MARCHE Claude committed
641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662
\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}

663
\bibliographystyle{plain}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
664
\bibliography{manual}
665
%\bibliography{abbrevs,demons,demons2,demons3,team,crossrefs}
666

MARCHE Claude's avatar
MARCHE Claude committed
667

MARCHE Claude's avatar
MARCHE Claude committed
668 669 670
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
671 672
\cleardoublepage
\listoffigures
673 674 675
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
676
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
677 678 679 680 681 682

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