manual.tex 9.94 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
\input{./myhevea.tex}
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
%HEVEA \newstyle{table.lstframe}{width:100\%;border-width:1px;}
42

MARCHE Claude's avatar
MARCHE Claude committed
43 44 45 46 47 48
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
50
% for ocamldoc generated pages
51
%\usepackage{ocamldoc}
52 53
%\let\tt\ttfamily
%\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
54

MARCHE Claude's avatar
MARCHE Claude committed
55 56
\usepackage{ifthen}
\input{./macros.tex}
57
\input{./replayer_macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
58

MARCHE Claude's avatar
MARCHE Claude committed
59 60
\input{./version.tex}

61 62
\makeindex

63 64
%HEVEA\title{The Why3 platform}

MARCHE Claude's avatar
MARCHE Claude committed
65
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
66
\sloppy
67
%BEGIN LATEX
68
\hbadness=5000
69
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
70

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
71 72 73 74
\thispagestyle{empty}

\begin{center}

75
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
76
\rule\textwidth{0.8mm}
77
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
78 79 80

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
81 82 83 84 85 86
{
%BEGIN LATEX
\fontsize{40}{40pt}\selectfont
%END LATEX
%HEVEA \Huge
\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
87 88 89

\vfill

90
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
91
\rule\textwidth{0.8mm}
92
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
93 94 95

\vfill

96
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
97

98
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
99
\begin{LARGE}
100
%END LATEX
101
  Version \whyversion{}, March 2013
102
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
103
\end{LARGE}
104
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
105 106 107

\vfill

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

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
125
\begin{tabular}{l}
126 127
$^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
128 129
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
130
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
131
\bigskip
MARCHE Claude's avatar
MARCHE Claude committed
132
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
133

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

136
\urldef{\urlutcat}{\url}{http://frama-c.com/u3cat/}
137 138
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}

139 140 141 142 143
  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
144 145 146

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
148 149
\chapter*{Foreword}

150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166
%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
167 168 169 170 171
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
172

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
173
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
174

MARCHE Claude's avatar
MARCHE Claude committed
175 176 177
\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
178

MARCHE Claude's avatar
MARCHE Claude committed
179
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
180 181 182
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
183
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
184 185
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
186
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
187 188 189 190

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


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

MARCHE Claude's avatar
MARCHE Claude committed
197
We gratefully thank the people who contributed to \why, directly or
198 199
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
200

201 202 203 204 205 206 207 208 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 240 241 242 243 244 245 246
\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}

\input{realizations.tex}

\input{coq_tactic.tex}

% \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
247

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

250 251
The syntax of \whyml programs changed in release 0.80. 
The table in Figure~\ref{fig:syntax080} summarizes the changes.
252

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
349
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
350 351 352 353 354 355 356 357 358
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
359
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
360 361 362 363 364
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
365
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
366 367 368
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
369

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

373
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
374 375 376 377 378 379 380 381
  \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}
382

MARCHE Claude's avatar
MARCHE Claude committed
383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404
\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
405
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
406 407
\bibliography{manual}
%\input{biblio-demons}
408

MARCHE Claude's avatar
MARCHE Claude committed
409

MARCHE Claude's avatar
MARCHE Claude committed
410 411 412
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
413 414
\cleardoublepage
\listoffigures
415 416 417
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
418
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
419 420 421 422 423 424

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