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

52 53
%HEVEA\title{The Why3 platform}

MARCHE Claude's avatar
MARCHE Claude committed
54
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
55
\sloppy
56
%BEGIN LATEX
57
\hbadness=5000
58
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
59

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
60 61 62 63
\thispagestyle{empty}

\begin{center}

64
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
65
\rule\textwidth{0.8mm}
66
%END LATEX
MARCHE Claude's avatar
MARCHE Claude committed
67 68 69

\vfill

70 71 72 73 74 75
\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
76 77 78

\vfill

79
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
80
\rule\textwidth{0.8mm}
81
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
82 83 84

\vfill

85
\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
86

87
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
88
\begin{LARGE}
89
%END LATEX
90
  Version \whyversion{}, May 2012
91
%BEGIN LATEX
MARCHE Claude's avatar
MARCHE Claude committed
92
\end{LARGE}
93
%END LATEX
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
94 95 96

\vfill

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

\begin{flushleft}

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

119
\begin{latexonly}
MARCHE Claude's avatar
MARCHE Claude committed
120
\bigskip
121
\end{latexonly}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
122

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

125 126 127 128 129 130 131
\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
132 133 134 135
  System@tic competitivity cluster.

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
137 138
\chapter*{Foreword}

MARCHE Claude's avatar
MARCHE Claude committed
139
This is the manual for the Why platform version 3, or \why for
140 141 142 143 144 145 146 147
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
148

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
149
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
150

MARCHE Claude's avatar
MARCHE Claude committed
151 152 153
\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
154

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

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
162
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
163 164 165 166

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


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

MARCHE Claude's avatar
MARCHE Claude committed
173
We gratefully thank the people who contributed to \why, directly or
174 175
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
176

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

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

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

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

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

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

237
\begin{latexonly}
MARCHE Claude's avatar
MARCHE Claude committed
238
\tableofcontents
239
\end{latexonly}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
240

241
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
242

MARCHE Claude's avatar
MARCHE Claude committed
243 244
\part{Tutorial}

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

MARCHE Claude's avatar
doc  
MARCHE Claude committed
247
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
248

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

251
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
252

MARCHE Claude's avatar
doc  
MARCHE Claude committed
253 254
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
255 256
\part{Reference Manual}

257 258 259 260
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
261 262 263 264
\input{syntaxref.tex}

\input{library.tex}

265 266
\input{realizations.tex}

267
\input{coq_tactic.tex}
268

269 270
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
271

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

274 275 276 277
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
278
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
279 280
\bibliography{manual}
%\input{biblio-demons}
281

MARCHE Claude's avatar
MARCHE Claude committed
282

MARCHE Claude's avatar
MARCHE Claude committed
283 284 285
% \cleardoublepage
% \input{glossary.tex}

MARCHE Claude's avatar
MARCHE Claude committed
286 287
\cleardoublepage
\listoffigures
288 289 290
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
291
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
292 293 294 295 296 297

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