manual.tex 6.51 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}

MARCHE Claude's avatar
MARCHE Claude committed
7 8 9
% tells memoir style to number subsections
\setsecnumdepth{subsection}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
10
\usepackage[T1]{fontenc}
11
\usepackage{lmodern}
12
%\usepackage{url}
13
\usepackage[pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
MARCHE Claude's avatar
MARCHE Claude committed
14
\usepackage{graphicx}
15
\usepackage{listings}
MARCHE Claude's avatar
MARCHE Claude committed
16
\usepackage{xspace}
17
\usepackage{hevea}
MARCHE Claude's avatar
MARCHE Claude committed
18

MARCHE Claude's avatar
MARCHE Claude committed
19 20 21 22 23
\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
\setheadfoot{15pt}{38pt}
\checkandfixthelayout

MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27 28 29 30
% placement of figures
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}
\setcounter{topnumber}{4}
\setcounter{bottomnumber}{4}
\setcounter{totalnumber}{8}
MARCHE Claude's avatar
MARCHE Claude committed
31

MARCHE Claude's avatar
MARCHE Claude committed
32 33 34 35 36 37
% \usepackage[toc,nonumberlist]{glossaries}
% \makeglossaries

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
39
% for ocamldoc generated pages
40
%\usepackage{ocamldoc}
41 42
%\let\tt\ttfamily
%\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
43

MARCHE Claude's avatar
MARCHE Claude committed
44 45
\usepackage{ifthen}
\input{./macros.tex}
46
\input{./replayer_macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
47

MARCHE Claude's avatar
MARCHE Claude committed
48 49
\input{./version.tex}

50 51
\makeindex

MARCHE Claude's avatar
MARCHE Claude committed
52
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
53
\sloppy
54
\hbadness=5000
MARCHE Claude's avatar
MARCHE Claude committed
55

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
56 57 58 59
\thispagestyle{empty}

\begin{center}

MARCHE Claude's avatar
MARCHE Claude committed
60 61 62 63
\rule\textwidth{0.8mm}

\vfill

64 65
{\Huge\fontsize{40}{40pt}
\selectfont\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
66 67 68

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
69
\rule\textwidth{0.8mm}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
70 71 72

\vfill

73
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
74 75


MARCHE Claude's avatar
MARCHE Claude committed
76
\begin{LARGE}
77
  Version \whyversion{}, May 2012
MARCHE Claude's avatar
MARCHE Claude committed
78
\end{LARGE}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
79 80 81

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
82 83
\begin{Large}
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
84 85 86
  Fran\c{c}ois Bobot$^{1,2}$ \\
  Jean-Christophe Filli\^atre$^{1,2}$  \\
  Claude March\'e$^{2,1}$ \\
87
  Guillaume Melquiond$^{2,1}$\\
MARCHE Claude's avatar
MARCHE Claude committed
88
  Andrei Paskevich$^{1,2}$
MARCHE Claude's avatar
MARCHE Claude committed
89 90 91 92 93 94
\end{tabular}
\end{Large}
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
95
\begin{tabular}{l}
MARCHE Claude's avatar
MARCHE Claude committed
96
$^1$ LRI, CNRS, Univ Paris-Sud, Orsay, F-91405 \\
Guillaume Melquiond's avatar
Guillaume Melquiond committed
97
$^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
98 99
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
100
\bigskip
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
101

102
  \textcopyright 2010-2012 Univ Paris-Sud, CNRS, INRIA
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
103

MARCHE Claude's avatar
MARCHE Claude committed
104
  This work has been partly supported by the `U3CAT' national ANR project
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
105 106 107 108 109 110
  (ANR-08-SEGI-021-08, \url{http://frama-c.cea.fr/u3cat}) and by the
  Hi-Lite (\url{http://www.open-do.org/projects/hi-lite/}) FUI project of the
  System@tic competitivity cluster.

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
112 113
\chapter*{Foreword}

MARCHE Claude's avatar
MARCHE Claude committed
114
This is the manual for the Why platform version 3, or \why for
115 116 117 118 119 120 121 122
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
123

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
124
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
125

MARCHE Claude's avatar
MARCHE Claude committed
126 127 128
\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
129

MARCHE Claude's avatar
MARCHE Claude committed
130
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
131 132 133
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
134
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
135 136
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
137
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
138 139 140 141

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


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

MARCHE Claude's avatar
MARCHE Claude committed
148
We gratefully thank the people who contributed to \why, directly or
149 150
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
151

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
154
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
155 156 157 158 159 160 161 162 163
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
164
  \item declarations are structured in components called ``theories'',
MARCHE Claude's avatar
MARCHE Claude committed
165 166 167 168 169
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
170
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
171 172 173
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
174

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

178
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
179 180 181 182 183 184 185 186
  \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}
187

MARCHE Claude's avatar
MARCHE Claude committed
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
\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
210 211 212 213
\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
214

215
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
216

MARCHE Claude's avatar
MARCHE Claude committed
217 218
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
219 220
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
221
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
222

MARCHE Claude's avatar
MARCHE Claude committed
223
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
224

225
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
226

MARCHE Claude's avatar
doc  
MARCHE Claude committed
227 228
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
229 230
\part{Reference Manual}

231 232 233 234
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
235 236 237 238
\input{syntaxref.tex}

\input{library.tex}

239 240
\input{realizations.tex}

241
\input{coq_tactic.tex}
242

243 244
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
245

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

248 249 250 251
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
252
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
253 254
\bibliography{manual}
%\input{biblio-demons}
255

MARCHE Claude's avatar
MARCHE Claude committed
256

MARCHE Claude's avatar
MARCHE Claude committed
257 258 259
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
260 261
\cleardoublepage
\listoffigures
262 263 264
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
265
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
266 267 268 269 270 271

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