manual.tex 6.05 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
biblio  
MARCHE Claude committed
5
\usepackage[T1]{fontenc}
6
\usepackage{lmodern}
7 8
%\usepackage{url}
\usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
MARCHE Claude's avatar
MARCHE Claude committed
9
\usepackage{graphicx}
MARCHE Claude's avatar
MARCHE Claude committed
10
\usepackage{xspace}
MARCHE Claude's avatar
MARCHE Claude committed
11

MARCHE Claude's avatar
MARCHE Claude committed
12 13 14 15 16
\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
\setheadfoot{15pt}{38pt}
\checkandfixthelayout

MARCHE Claude's avatar
MARCHE Claude committed
17 18 19 20 21 22 23
% 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
24

25 26
%\usepackage[toc,nonumberlist]{glossaries}
%\makeglossaries
Andrei Paskevich's avatar
Andrei Paskevich committed
27

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
28
% for ocamldoc generated pages
29
%\usepackage{ocamldoc}
MARCHE Claude's avatar
MARCHE Claude committed
30 31
\let\tt\ttfamily
\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
32

MARCHE Claude's avatar
MARCHE Claude committed
33 34
\usepackage{ifthen}
\input{./macros.tex}
35
\input{./replayer_macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
36

MARCHE Claude's avatar
MARCHE Claude committed
37 38
\input{./version.tex}

39 40
\makeindex

MARCHE Claude's avatar
MARCHE Claude committed
41
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
42
\sloppy
MARCHE Claude's avatar
MARCHE Claude committed
43
\hbadness=1000
MARCHE Claude's avatar
MARCHE Claude committed
44

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
45 46 47 48
\thispagestyle{empty}

\begin{center}

MARCHE Claude's avatar
MARCHE Claude committed
49 50 51 52 53
\rule\textwidth{0.8mm}

\vfill

{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
54 55 56

\vfill

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

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
61
\begin{LARGE}
MARCHE Claude's avatar
MARCHE Claude committed
62
  Version \whyversion{}, October 2011
MARCHE Claude's avatar
MARCHE Claude committed
63
\end{LARGE}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
64 65 66

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
67 68
\begin{Large}
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
69 70 71 72
  Fran\c{c}ois Bobot$^{1,2}$ \\
  Jean-Christophe Filli\^atre$^{1,2}$  \\
  Claude March\'e$^{2,1}$ \\
  Andrei Paskevich$^{1,2}$
MARCHE Claude's avatar
MARCHE Claude committed
73 74 75 76 77 78
\end{tabular}
\end{Large}
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
79
\begin{tabular}{l}
MARCHE Claude's avatar
MARCHE Claude committed
80 81
$^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
82 83
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
84
\bigskip
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
85

86
  \textcopyright 2010-2011 Univ Paris-Sud, CNRS, INRIA
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
87

MARCHE Claude's avatar
MARCHE Claude committed
88
  This work has been partly supported by the `U3CAT' national ANR project
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
89 90 91 92 93 94
  (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
95

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
96 97
\chapter*{Foreword}

MARCHE Claude's avatar
MARCHE Claude committed
98
This is the manual for the Why platform version 3, or \why for
99 100 101 102 103 104 105 106
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
107

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
108
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
109

MARCHE Claude's avatar
MARCHE Claude committed
110 111 112
\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
113

MARCHE Claude's avatar
MARCHE Claude committed
114
\why is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
115 116 117
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
118
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
119 120
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
121
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
122 123 124 125

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


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

MARCHE Claude's avatar
MARCHE Claude committed
132 133
We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Simon Cruanes, Johannes Kanig, St\'ephane
MARCHE Claude's avatar
MARCHE Claude committed
134 135
Lescuyer, Sim\~ao Melo de Sousa, Guillaume Melquiond, Benjamin Monate,
Asma Tafat.
MARCHE Claude's avatar
MARCHE Claude committed
136

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
139
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
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
  \item declarations are structured in components called "theories",
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
155
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
156 157 158 159
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}
\item Source code organized as a library with a documented API, to
MARCHE Claude's avatar
MARCHE Claude committed
160
  allow access to \why features programmatically.
MARCHE Claude's avatar
MARCHE Claude committed
161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192

\item GUI with new features w.r.t. the former GWhy
  \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}
\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
193 194 195 196
\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
197

198
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
199

MARCHE Claude's avatar
MARCHE Claude committed
200 201
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
202 203
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
204
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
205

MARCHE Claude's avatar
MARCHE Claude committed
206
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
207

208
\input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
209

MARCHE Claude's avatar
doc  
MARCHE Claude committed
210 211
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
212 213
\part{Reference Manual}

214
% \input{glossary.tex}
Andrei Paskevich's avatar
Andrei Paskevich committed
215

MARCHE Claude's avatar
MARCHE Claude committed
216 217 218 219
\input{syntaxref.tex}

\input{library.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
220 221
\input{manpages.tex}

222 223
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
224

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

MARCHE Claude's avatar
MARCHE Claude committed
227
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
228 229
\bibliography{manual}
%\input{biblio-demons}
230

MARCHE Claude's avatar
MARCHE Claude committed
231 232 233

\cleardoublepage
\listoffigures
234 235 236
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
237
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
238 239 240 241 242 243

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