manual.tex 7.08 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
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
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
MARCHE Claude committed
56

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
MARCHE Claude committed
69 70 71 72
\thispagestyle{empty}

\begin{center}

73
%BEGIN LATEX
74
\rule\textwidth{0.8mm}
75
%END LATEX
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
MARCHE Claude committed
85 86 87

\vfill

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

\vfill

94
\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
95

96
%BEGIN LATEX
97
\begin{LARGE}
98
%END LATEX
99
  Version \whyversion{}, October 2012
100
%BEGIN LATEX
101
\end{LARGE}
102
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
103 104 105

\vfill

106
%BEGIN LATEX
107
\begin{Large}
108
%END LATEX
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}$
115
\end{tabular}
116
%BEGIN LATEX
117
\end{Large}
118
%END LATEX
119 120 121 122
\vfill

\begin{flushleft}

MARCHE Claude's avatar
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
MARCHE Claude committed
126 127
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
128
%BEGIN LATEX
129
\bigskip
MARCHE Claude's avatar
MARCHE Claude committed
130
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
131

132
  \textcopyright 2010-2012 Univ Paris-Sud, CNRS, Inria
MARCHE Claude's avatar
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
MARCHE Claude committed
142 143 144

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

MARCHE Claude's avatar
MARCHE Claude committed
146 147
\chapter*{Foreword}

MARCHE Claude's avatar
MARCHE Claude committed
148
This is the manual for the Why platform version 3, or \why for
149 150 151 152 153 154 155 156
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
MARCHE Claude committed
157

MARCHE Claude's avatar
MARCHE Claude committed
158
\subsection*{Availability}
159

MARCHE Claude's avatar
MARCHE Claude committed
160 161 162
\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.
163

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

MARCHE Claude's avatar
MARCHE Claude committed
171
\subsection*{Contact}
172 173 174 175

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
176
Report any bug to the \why Bug Tracking System:
177 178 179
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.


Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
180
\subsection*{Acknowledgements}
181

MARCHE Claude's avatar
MARCHE Claude committed
182
We gratefully thank the people who contributed to \why, directly or
183 184
indirectly: Romain Bardou, Simon Cruanes, Leon Gondelman, Johannes Kanig,
St\'ephane Lescuyer, Sim\~ao Melo de Sousa, Benjamin Monate, Asma Tafat.
185

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
186
\subsection*{Summary of Changes w.r.t. Why 2}
MARCHE Claude's avatar
MARCHE Claude committed
187

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

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
204
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
205 206 207
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
208

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

212
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
213 214 215 216 217 218 219 220
  \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}
221

MARCHE Claude's avatar
MARCHE Claude committed
222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243
\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}

244 245
\cleardoublepage

MARCHE Claude's avatar
MARCHE Claude committed
246
%BEGIN LATEX
247
\tableofcontents
MARCHE Claude's avatar
MARCHE Claude committed
248
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
249

250
%\input{intro.tex}
251

MARCHE Claude's avatar
MARCHE Claude committed
252 253
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
254 255
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
256
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
257

MARCHE Claude's avatar
MARCHE Claude committed
258
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
259

260
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
261

MARCHE Claude's avatar
doc  
MARCHE Claude committed
262 263
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
264 265
\part{Reference Manual}

266 267 268 269
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
270 271 272 273
\input{syntaxref.tex}

\input{library.tex}

274 275
\input{realizations.tex}

276
\input{coq_tactic.tex}
277

278 279
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
280

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

283 284 285 286
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
287
\bibliographystyle{abbrv}
MARCHE Claude's avatar
MARCHE Claude committed
288 289
\bibliography{manual}
%\input{biblio-demons}
290

MARCHE Claude's avatar
MARCHE Claude committed
291

MARCHE Claude's avatar
MARCHE Claude committed
292 293 294
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
295 296
\cleardoublepage
\listoffigures
297 298 299
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
300
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
301 302 303 304 305 306

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