manual.tex 6.34 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 11
%\usepackage{url}
\usepackage[a4paper,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}
MARCHE Claude's avatar
MARCHE Claude committed
15

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

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

29 30
%\usepackage[toc,nonumberlist]{glossaries}
%\makeglossaries
Andrei Paskevich's avatar
Andrei Paskevich committed
31

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
32
% for ocamldoc generated pages
33
%\usepackage{ocamldoc}
MARCHE Claude's avatar
MARCHE Claude committed
34 35
\let\tt\ttfamily
\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
36

MARCHE Claude's avatar
MARCHE Claude committed
37 38
\usepackage{ifthen}
\input{./macros.tex}
39
\input{./replayer_macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
40

MARCHE Claude's avatar
MARCHE Claude committed
41 42
\input{./version.tex}

43 44
\makeindex

MARCHE Claude's avatar
MARCHE Claude committed
45
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
46
\sloppy
47
\hbadness=5000
MARCHE Claude's avatar
MARCHE Claude committed
48

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
49 50 51 52
\thispagestyle{empty}

\begin{center}

MARCHE Claude's avatar
MARCHE Claude committed
53 54 55 56 57
\rule\textwidth{0.8mm}

\vfill

{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
58 59 60

\vfill

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

\vfill

65
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
66 67


MARCHE Claude's avatar
MARCHE Claude committed
68
\begin{LARGE}
69
  Version \whyversion{}, May 2012
MARCHE Claude's avatar
MARCHE Claude committed
70
\end{LARGE}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
71 72 73

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
74 75
\begin{Large}
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
76 77 78
  Fran\c{c}ois Bobot$^{1,2}$ \\
  Jean-Christophe Filli\^atre$^{1,2}$  \\
  Claude March\'e$^{2,1}$ \\
79
  Guillaume Melquiond$^{2,1}$\\
MARCHE Claude's avatar
MARCHE Claude committed
80
  Andrei Paskevich$^{1,2}$
MARCHE Claude's avatar
MARCHE Claude committed
81 82 83 84 85 86
\end{tabular}
\end{Large}
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
87
\begin{tabular}{l}
MARCHE Claude's avatar
MARCHE Claude committed
88 89
$^1$ LRI, CNRS, Univ Paris-Sud, Orsay, F-91405 \\
$^2$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
90 91
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
92
\bigskip
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
93

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

MARCHE Claude's avatar
MARCHE Claude committed
96
  This work has been partly supported by the `U3CAT' national ANR project
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
97 98 99 100 101 102
  (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
103

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
104 105
\chapter*{Foreword}

MARCHE Claude's avatar
MARCHE Claude committed
106
This is the manual for the Why platform version 3, or \why for
107 108 109 110 111 112 113 114
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
115

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
116
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
117

MARCHE Claude's avatar
MARCHE Claude committed
118 119 120
\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
121

MARCHE Claude's avatar
MARCHE Claude committed
122
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
123 124 125
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
126
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
127 128
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
129
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
130 131 132 133

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


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

MARCHE Claude's avatar
MARCHE Claude committed
140
We gratefully thank the people who contributed to \why, directly or
141 142
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
143

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

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

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
162
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
163 164 165
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
166

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

170
\item GUI with new features with respect to the former GWhy
MARCHE Claude's avatar
MARCHE Claude committed
171 172 173 174 175 176 177 178
  \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}
179

MARCHE Claude's avatar
MARCHE Claude committed
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
\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
202 203 204 205
\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
206

207
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
208

MARCHE Claude's avatar
MARCHE Claude committed
209 210
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
211 212
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
213
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
214

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
221 222
\part{Reference Manual}

223
% \input{glossary.tex}
Andrei Paskevich's avatar
Andrei Paskevich committed
224

225 226 227 228
\input{install.tex}

\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
229 230 231 232
\input{syntaxref.tex}

\input{library.tex}

233 234
\input{realizations.tex}

235
\input{coq_tactic.tex}
236

237 238
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
239

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

242 243 244 245
% \appendix

\input{technical.tex}

MARCHE Claude's avatar
MARCHE Claude committed
246
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
247 248
\bibliography{manual}
%\input{biblio-demons}
249

MARCHE Claude's avatar
MARCHE Claude committed
250 251 252

\cleardoublepage
\listoffigures
253 254 255
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
256
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
257 258 259 260 261 262

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