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

199 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 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266
\subsection*{Release Notes for version 0.80: Syntax Changes w.r.t. 0.73}

The syntax of \texttt{mlw} programms changed in release 0.80, with respect to release 0.73. The table of Figure~\ref{fig:syntax080} summaries these changes.

\begin{figure}[t]
  \centering
\begin{tabular}{|l|l|}
\hline
version 0.73 & version 0.80 \\
\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
let f (x:int) (y:int) : t = \\
\hspace*{3ex} \{ P \} \\
\hspace*{3ex} e \\
\hspace*{3ex} \{ Q \} \\
\hspace*{3ex} | Exc -> \{ R \} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
let f (x:int) (y:int) : t \\
\hspace*{3ex} requires \{ P \} \\
\hspace*{3ex} ensures \{ Q \} \\
\hspace*{3ex} raises \{ Exc -> R \} \\
\hspace*{3ex} = e \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
val f (x:int) (y:int) : \\
\hspace*{3ex} \{ P \} \\
\hspace*{3ex} t \\
\hspace*{3ex} writes a b \\
\hspace*{3ex} \{ Q \} \\
\hspace*{3ex} | Exc -> \{ R \} \\
\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 \{ Exc -> R \} \\
\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}

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
267
\subsection*{Summary of Changes w.r.t. Why 2}
MARCHE Claude's avatar
MARCHE Claude committed
268

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
269
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
270 271 272 273 274 275 276 277 278
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
279
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
280 281 282 283 284
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
285
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
286 287 288
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
289

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

293
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
294 295 296 297 298 299 300 301
  \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}
302

MARCHE Claude's avatar
MARCHE Claude committed
303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324
\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
325 326
\cleardoublepage

MARCHE Claude's avatar
MARCHE Claude committed
327
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
328
\tableofcontents
MARCHE Claude's avatar
MARCHE Claude committed
329
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
330

331
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
332

MARCHE Claude's avatar
MARCHE Claude committed
333 334
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
335 336
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
337
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
338

MARCHE Claude's avatar
MARCHE Claude committed
339
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
340

341
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
342

MARCHE Claude's avatar
doc  
MARCHE Claude committed
343 344
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
345 346
\part{Reference Manual}

347 348 349 350
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
351 352 353 354
\input{syntaxref.tex}

\input{library.tex}

355 356
\input{realizations.tex}

357
\input{coq_tactic.tex}
358

359 360
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
361

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

364 365 366 367
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
368
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
369 370
\bibliography{manual}
%\input{biblio-demons}
371

MARCHE Claude's avatar
MARCHE Claude committed
372

MARCHE Claude's avatar
MARCHE Claude committed
373 374 375
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
376 377
\cleardoublepage
\listoffigures
378 379 380
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
381
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
382 383 384 385 386 387

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