manual.tex 6.49 KB
Newer Older
1
\documentclass[a4paper,11pt,twoside,openright]{memoir}
MARCHE Claude's avatar
MARCHE Claude committed
2

3 4
% rubber: module index

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25 26 27 28
% 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
29

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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
46 47
\input{./version.tex}

48 49
\makeindex

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
54 55 56 57
\thispagestyle{empty}

\begin{center}

MARCHE Claude's avatar
MARCHE Claude committed
58 59 60 61
\rule\textwidth{0.8mm}

\vfill

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

\vfill

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

\vfill

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


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

\vfill

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

\begin{flushleft}

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

MARCHE Claude's avatar
MARCHE Claude committed
98
\bigskip
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
99

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

MARCHE Claude's avatar
MARCHE Claude committed
102
  This work has been partly supported by the `U3CAT' national ANR project
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
103 104 105 106 107 108
  (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
109

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
110 111
\chapter*{Foreword}

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

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
122
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
123

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

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

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

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


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

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

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

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

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

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

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

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

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
212

213
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
214

MARCHE Claude's avatar
MARCHE Claude committed
215 216
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
217 218
\input{starting.tex}

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

MARCHE Claude's avatar
MARCHE Claude committed
221
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
222

223
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
224

MARCHE Claude's avatar
doc  
MARCHE Claude committed
225 226
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
227 228
\part{Reference Manual}

229 230 231 232
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
233 234 235 236
\input{syntaxref.tex}

\input{library.tex}

237 238
\input{realizations.tex}

239
\input{coq_tactic.tex}
240

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

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

246 247 248 249
% \appendix

\input{technical.tex}

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

MARCHE Claude's avatar
MARCHE Claude committed
254

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

MARCHE Claude's avatar
MARCHE Claude committed
258 259
\cleardoublepage
\listoffigures
260 261 262
\cleardoublepage
\printindex

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

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