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

%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
25
\usepackage{graphicx}
MARCHE Claude's avatar
MARCHE Claude committed
26 27 28
%END LATEX
%HEVEA \newcommand{\includegraphics}[2][2]{\imgsrc{#2}}

29
\usepackage{listings}
MARCHE Claude's avatar
MARCHE Claude committed
30
\usepackage{xspace}
MARCHE Claude's avatar
MARCHE Claude committed
31

32
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
33 34 35 36 37
\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
\setheadfoot{15pt}{38pt}
\checkandfixthelayout

MARCHE Claude's avatar
MARCHE Claude committed
38 39 40 41
% placement of figures
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}
42
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
43 44 45
\setcounter{topnumber}{4}
\setcounter{bottomnumber}{4}
\setcounter{totalnumber}{8}
MARCHE Claude's avatar
MARCHE Claude committed
46

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

MARCHE Claude's avatar
MARCHE Claude committed
49 50 51 52 53 54
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
56
% for ocamldoc generated pages
57
%\usepackage{ocamldoc}
58 59
%\let\tt\ttfamily
%\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
60

MARCHE Claude's avatar
MARCHE Claude committed
61 62
\usepackage{ifthen}
\input{./macros.tex}
63
\input{./replayer_macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
64

MARCHE Claude's avatar
MARCHE Claude committed
65 66
\input{./version.tex}

67 68
\makeindex

69 70
%HEVEA\title{The Why3 platform}

MARCHE Claude's avatar
MARCHE Claude committed
71
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
72
\sloppy
73
%BEGIN LATEX
74
\hbadness=5000
75
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
76

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
77 78 79 80
\thispagestyle{empty}

\begin{center}

81
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
82
\rule\textwidth{0.8mm}
83
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
84 85 86

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
87 88 89 90 91 92
{
%BEGIN LATEX
\fontsize{40}{40pt}\selectfont
%END LATEX
%HEVEA \Huge
\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
93 94 95

\vfill

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

\vfill

102
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
103

104
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
105
\begin{LARGE}
106
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
107
  Version \whyversion{}, December 2013
108
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
109
\end{LARGE}
110
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
111 112 113

\vfill

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

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
131
\begin{tabular}{l}
132 133
$^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
134 135
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
136
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
137
\bigskip
MARCHE Claude's avatar
MARCHE Claude committed
138
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
139

140
  \textcopyright 2010-2013 University Paris-Sud, CNRS, Inria
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
141

142
\urldef{\urlutcat}{\url}{http://frama-c.com/u3cat/}
143 144
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}

145 146 147 148 149
  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
150 151 152

\end{flushleft}
\end{center}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
153

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
154 155
\chapter*{Foreword}

156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
%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
173 174 175 176 177
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
178

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
179
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
180

MARCHE Claude's avatar
MARCHE Claude committed
181 182 183
\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
184

MARCHE Claude's avatar
MARCHE Claude committed
185
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
186 187 188
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
189
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
190 191
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
192
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
193 194 195 196

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


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

MARCHE Claude's avatar
MARCHE Claude committed
203
We gratefully thank the people who contributed to \why, directly or
MARCHE Claude's avatar
MARCHE Claude committed
204 205 206 207 208
indirectly: Romain Bardou, Stefan Berghofer, Sylvie Boldo, Martin
Clochard, Simon Cruanes, Leon Gondelman, Johannes Kanig, St\'ephane
Lescuyer, David Mentr\'e, Sim\~ao Melo de Sousa, Benjamin Monate,
Thi-Minh-Tuyen Nguyen, Asma Tafat, Piotr Trojanek.

MARCHE Claude's avatar
MARCHE Claude committed
209

210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239
\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}

\input{library.tex}

240
\input{itp.tex}
241 242 243 244 245 246 247 248 249 250 251 252 253 254


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

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

\input{technical.tex}

\part{Appendix}

\appendix

\chapter{Release Notes}
MARCHE Claude's avatar
MARCHE Claude committed
255

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

258 259
The syntax of \whyml programs changed in release 0.80. 
The table in Figure~\ref{fig:syntax080} summarizes the changes.
260

261
\begin{figure}[thbp]
262
  \centering
263
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
264
\hline
265 266
\textbf{version 0.73} & \textbf{version 0.80} \\
\hline
267 268
\ttfamily
type t = \{| field~:~int |\}
269
&
270 271
\ttfamily
type t = \{ field~:~int \}
272 273
\\
\hline
274 275
\ttfamily
\{| field = 5 |\}
276
&
277 278
\ttfamily
\{ field = 5 \}
279
\\
280
\hline
281 282
\ttfamily
use import module M
283
&
284 285
\ttfamily
use import M
286 287
\\
\hline
288 289 290 291 292 293 294 295
\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 \}
296
&
297 298 299 300 301 302 303 304
\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
305 306
\\
\hline
307 308 309 310 311 312 313 314
\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 \}
315
&
316 317 318 319 320 321 322
\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 \}
323 324
\\
\hline
325 326 327 328 329 330 331 332
\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 \}
333
&
334 335 336 337 338 339 340
\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 \}
341 342
\\
\hline
343 344
\ttfamily
abstract e \{ Q \}
345
&
346 347
\ttfamily
abstract e ensures \{ Q \}
348 349 350 351 352 353 354
\\
\hline
\end{tabular}
\caption{Syntax changes from version 0.73 to version 0.80}
\label{fig:syntax080}
\end{figure}

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
357
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
358 359 360 361 362 363 364 365 366
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
367
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
368 369 370 371 372
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
373
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
374 375 376
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
377

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

381
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
382 383 384 385 386 387 388 389
  \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}
390

MARCHE Claude's avatar
MARCHE Claude committed
391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412
\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
413
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
414 415
\bibliography{manual}
%\input{biblio-demons}
416

MARCHE Claude's avatar
MARCHE Claude committed
417

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

MARCHE Claude's avatar
MARCHE Claude committed
421 422
\cleardoublepage
\listoffigures
423 424 425
\cleardoublepage
\printindex

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

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