manual.tex 7.09 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
\usepackage{graphicx}
17
\usepackage{listings}
MARCHE Claude's avatar
MARCHE Claude committed
18
\usepackage{xspace}
19
\usepackage{hevea}
MARCHE Claude's avatar
MARCHE Claude committed
20

21
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25 26
\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
\setheadfoot{15pt}{38pt}
\checkandfixthelayout

MARCHE Claude's avatar
MARCHE Claude committed
27 28 29 30
% placement of figures
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}
31
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
32 33 34
\setcounter{topnumber}{4}
\setcounter{bottomnumber}{4}
\setcounter{totalnumber}{8}
MARCHE Claude's avatar
MARCHE Claude committed
35

MARCHE Claude's avatar
MARCHE Claude committed
36 37 38 39 40 41
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
43
% for ocamldoc generated pages
44
%\usepackage{ocamldoc}
45 46
%\let\tt\ttfamily
%\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
47

MARCHE Claude's avatar
MARCHE Claude committed
48 49
\usepackage{ifthen}
\input{./macros.tex}
50
\input{./replayer_macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
51

MARCHE Claude's avatar
MARCHE Claude committed
52 53
\input{./version.tex}

54 55
\makeindex

56 57
%HEVEA\title{The Why3 platform}

MARCHE Claude's avatar
MARCHE Claude committed
58
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
59
\sloppy
60
%BEGIN LATEX
61
\hbadness=5000
62
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
63

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
64 65 66 67
\thispagestyle{empty}

\begin{center}

68
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
69
\rule\textwidth{0.8mm}
70
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
71 72 73

\vfill

74 75 76 77 78 79
\begin{latexonly}
{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}
\end{latexonly}
\begin{htmlonly}
{\Huge\bfseries\sffamily The Why3 platform}
\end{htmlonly}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
80 81 82

\vfill

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

\vfill

89
\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
90

91
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
92
\begin{LARGE}
93
%END LATEX
94
  Version \whyversion{}, October 2012
95
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
96
\end{LARGE}
97
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
98 99 100

\vfill

101
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
102
\begin{Large}
103
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
104
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
105 106 107
  Fran\c{c}ois Bobot$^{1,2}$ \\
  Jean-Christophe Filli\^atre$^{1,2}$  \\
  Claude March\'e$^{2,1}$ \\
108
  Guillaume Melquiond$^{2,1}$\\
MARCHE Claude's avatar
MARCHE Claude committed
109
  Andrei Paskevich$^{1,2}$
MARCHE Claude's avatar
MARCHE Claude committed
110
\end{tabular}
111
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
112
\end{Large}
113
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
114 115 116 117
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
118
\begin{tabular}{l}
MARCHE Claude's avatar
MARCHE Claude committed
119
$^1$ LRI, CNRS, Univ Paris-Sud, Orsay, F-91405 \\
Guillaume Melquiond's avatar
Guillaume Melquiond committed
120
$^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
121 122
\end{tabular}

123
\begin{latexonly}
MARCHE Claude's avatar
MARCHE Claude committed
124
\bigskip
125
\end{latexonly}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
126

127
  \textcopyright 2010-2012 Univ Paris-Sud, CNRS, Inria
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
128

129 130 131 132 133 134 135
\urldef{\urlutcat}{\url}{http://frama-c.cea.fr/u3cat}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}

  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
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
136 137 138 139
  System@tic competitivity cluster.

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
141 142
\chapter*{Foreword}

MARCHE Claude's avatar
MARCHE Claude committed
143
This is the manual for the Why platform version 3, or \why for
144 145 146 147 148 149 150 151
short. \why is a complete reimplementation~\cite{boogie11why3} of the former Why
platform~\cite{filliatre07cav} for program
verification. Among the new features are: numerous
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
152

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
153
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
154

MARCHE Claude's avatar
MARCHE Claude committed
155 156 157
\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
158

MARCHE Claude's avatar
MARCHE Claude committed
159
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
160 161 162
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
163
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
164 165
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
166
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
167 168 169 170

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


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

MARCHE Claude's avatar
MARCHE Claude committed
177
We gratefully thank the people who contributed to \why, directly or
178 179
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
180

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
183
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
184 185 186 187 188 189 190 191 192
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
193
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
194 195 196 197 198
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
199
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
200 201 202
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
203

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

207
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
208 209 210 211 212 213 214 215
  \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}
216

MARCHE Claude's avatar
MARCHE Claude committed
217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238
\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
239 240
\cleardoublepage

241
\begin{latexonly}
MARCHE Claude's avatar
MARCHE Claude committed
242
\tableofcontents
243
\end{latexonly}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
244

245
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
246

MARCHE Claude's avatar
MARCHE Claude committed
247 248
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
249 250
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
251
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
252

MARCHE Claude's avatar
MARCHE Claude committed
253
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
254

255
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
256

MARCHE Claude's avatar
doc  
MARCHE Claude committed
257 258
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
259 260
\part{Reference Manual}

261 262 263 264
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
265 266 267 268
\input{syntaxref.tex}

\input{library.tex}

269 270
\input{realizations.tex}

271
\input{coq_tactic.tex}
272

273 274
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
275

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

278 279 280 281
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
282
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
283 284
\bibliography{manual}
%\input{biblio-demons}
285

MARCHE Claude's avatar
MARCHE Claude committed
286

MARCHE Claude's avatar
MARCHE Claude committed
287 288 289
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
290 291
\cleardoublepage
\listoffigures
292 293 294
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
295
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
296 297 298 299 300 301

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