manual.tex 10.5 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 208 209

\begin{figure}[t]
  \centering
\begin{tabular}{|l|l|}
\hline
210 211 212 213 214 215 216 217 218 219 220 221
\textbf{version 0.73} & \textbf{version 0.80} \\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
type t = \{| field~:~int |\} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
type t = \{ field~:~int \} \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
MARCHE Claude's avatar
MARCHE Claude committed
222
\{| field = 5 |\} \\
223 224 225
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
MARCHE Claude's avatar
MARCHE Claude committed
226
\{ field = 5 \} \\
227 228
\end{minipage}
\\
229 230 231 232 233 234 235 236 237 238 239
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
use import module M \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
use import M \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
240 241
let rec f (x:int) (y:int)~:~t 
\hspace*{3ex} variant \{ t \} with rel = \\
242 243 244
\hspace*{3ex} \{ P \} \\
\hspace*{3ex} e \\
\hspace*{3ex} \{ Q \} \\
245 246
\hspace*{3ex} | Exc1 -> \{ R1 \} \\
\hspace*{3ex} | Exc2 n -> \{ R2 \} \\
247 248 249
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
250 251
let rec f (x:int) (y:int)~:~t \\
\hspace*{3ex} variant \{ t with rel \}
252 253
\hspace*{3ex} requires \{ P \} \\
\hspace*{3ex} ensures \{ Q \} \\
254 255
\hspace*{3ex} raises \{ Exc1 -> R1 \\
\hspace*{3ex}~~~~~~~~| Exc2 n -> R2 \} \\
256 257 258 259 260
\hspace*{3ex} = e \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281
val f (x:int) (y:int)~:\\
\hspace*{3ex} \{ P \} \\
\hspace*{3ex} t \\
\hspace*{3ex} writes a b \\
\hspace*{3ex} \{ Q \} \\
\hspace*{3ex} | Exc1 -> \{ R1 \} \\
\hspace*{3ex} | Exc2 n -> \{ R2 \} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
val f (x:int) (y:int)~:~t \\
\hspace*{3ex} requires \{ P \} \\
\hspace*{3ex} writes \{ a, b \} \\
\hspace*{3ex} ensures \{ Q \} \\
\hspace*{3ex} raises \{ Exc1 -> R1 \\
\hspace*{3ex}~~~~~~~~| Exc2 n -> R2 \} \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
val f~:~x:int -> y:int ->\\
282 283 284 285
\hspace*{3ex} \{ P \} \\
\hspace*{3ex} t \\
\hspace*{3ex} writes a b \\
\hspace*{3ex} \{ Q \} \\
286 287
\hspace*{3ex} | Exc1 -> \{ R1 \} \\
\hspace*{3ex} | Exc2 n -> \{ R2 \} \\
288 289 290
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
291
val f (x y:int)~:~t \\
292 293 294
\hspace*{3ex} requires \{ P \} \\
\hspace*{3ex} writes \{ a, b \} \\
\hspace*{3ex} ensures \{ Q \} \\
295 296
\hspace*{3ex} raises \{ Exc1 -> R1 \\
\hspace*{3ex}~~~~~~~~| Exc2 n -> R2 \} \\
297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
abstract e \{ Q \} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
abstract e ensures \{ Q \} \\
\end{minipage}
\\
\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
314
\subsection{Summary of Changes w.r.t. Why 2}
MARCHE Claude's avatar
MARCHE Claude committed
315

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
316
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
317 318 319 320 321 322 323 324 325
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
326
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
327 328 329 330 331
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
332
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
333 334 335
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
336

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

340
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
341 342 343 344 345 346 347 348
  \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}
349

MARCHE Claude's avatar
MARCHE Claude committed
350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
\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
372 373
\cleardoublepage

MARCHE Claude's avatar
MARCHE Claude committed
374
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
375
\tableofcontents
MARCHE Claude's avatar
MARCHE Claude committed
376
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
377

378
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
379

MARCHE Claude's avatar
MARCHE Claude committed
380 381
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
382 383
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
384
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
385

MARCHE Claude's avatar
MARCHE Claude committed
386
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
387

388
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
389

MARCHE Claude's avatar
doc  
MARCHE Claude committed
390 391
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
392 393
\part{Reference Manual}

394 395 396 397
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
398 399 400 401
\input{syntaxref.tex}

\input{library.tex}

402 403
\input{realizations.tex}

404
\input{coq_tactic.tex}
405

406 407
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
408

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

411 412 413 414
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
415
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
416 417
\bibliography{manual}
%\input{biblio-demons}
418

MARCHE Claude's avatar
MARCHE Claude committed
419

MARCHE Claude's avatar
MARCHE Claude committed
420 421 422
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
423 424
\cleardoublepage
\listoffigures
425 426 427
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
428
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
429 430 431 432 433 434

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