manual.tex 9.86 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

MARCHE Claude's avatar
MARCHE Claude committed
199 200 201
\section{Release Notes}

\subsection{Release Notes for version 0.80: syntax changes w.r.t. 0.73}
202

203 204
The syntax of \whyml programs changed in release 0.80. 
The table in Figure~\ref{fig:syntax080} summarizes the changes.
205 206 207

\begin{figure}[t]
  \centering
208
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
209
\hline
210 211
\textbf{version 0.73} & \textbf{version 0.80} \\
\hline
212 213
\ttfamily
type t = \{| field~:~int |\}
214
&
215 216
\ttfamily
type t = \{ field~:~int \}
217 218
\\
\hline
219 220
\ttfamily
\{| field = 5 |\}
221
&
222 223
\ttfamily
\{ field = 5 \}
224
\\
225
\hline
226 227
\ttfamily
use import module M
228
&
229 230
\ttfamily
use import M
231 232
\\
\hline
233 234 235 236 237 238 239 240
\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 \}
241
&
242 243 244 245 246 247 248 249
\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
250 251
\\
\hline
252 253 254 255 256 257 258 259
\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 \}
260
&
261 262 263 264 265 266 267
\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 \}
268 269
\\
\hline
270 271 272 273 274 275 276 277
\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 \}
278
&
279 280 281 282 283 284 285
\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 \}
286 287
\\
\hline
288 289
\ttfamily
abstract e \{ Q \}
290
&
291 292
\ttfamily
abstract e ensures \{ Q \}
293 294 295 296 297 298 299
\\
\hline
\end{tabular}
\caption{Syntax changes from version 0.73 to version 0.80}
\label{fig:syntax080}
\end{figure}

MARCHE Claude's avatar
MARCHE Claude committed
300
\subsection{Summary of Changes w.r.t. Why 2}
MARCHE Claude's avatar
MARCHE Claude committed
301

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
302
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
303 304 305 306 307 308 309 310 311
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
312
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
313 314 315 316 317
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
318
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
319 320 321
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
322

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

326
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
327 328 329 330 331 332 333 334
  \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}
335

MARCHE Claude's avatar
MARCHE Claude committed
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357
\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
358 359
\cleardoublepage

MARCHE Claude's avatar
MARCHE Claude committed
360
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
361
\tableofcontents
MARCHE Claude's avatar
MARCHE Claude committed
362
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
363

364
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
365

MARCHE Claude's avatar
MARCHE Claude committed
366 367
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
368 369
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
370
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
371

MARCHE Claude's avatar
MARCHE Claude committed
372
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
373

374
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
375

MARCHE Claude's avatar
doc  
MARCHE Claude committed
376 377
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
378 379
\part{Reference Manual}

380 381 382 383
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
384 385 386 387
\input{syntaxref.tex}

\input{library.tex}

388 389
\input{realizations.tex}

390
\input{coq_tactic.tex}
391

392 393
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
394

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

397 398 399 400
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
401
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
402 403
\bibliography{manual}
%\input{biblio-demons}
404

MARCHE Claude's avatar
MARCHE Claude committed
405

MARCHE Claude's avatar
MARCHE Claude committed
406 407 408
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
409 410
\cleardoublepage
\listoffigures
411 412 413
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
414
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
415 416 417 418 419 420

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