manual.tex 5.98 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 7
%\usepackage{url}
\usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
MARCHE Claude's avatar
MARCHE Claude committed
8
\usepackage{graphicx}
MARCHE Claude's avatar
MARCHE Claude committed
9

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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
31 32
\usepackage{ifthen}
\input{./macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
33

MARCHE Claude's avatar
MARCHE Claude committed
34 35
\input{./version.tex}

36 37
\makeindex

MARCHE Claude's avatar
MARCHE Claude committed
38
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
39
\sloppy
MARCHE Claude's avatar
MARCHE Claude committed
40
\hbadness=1000
MARCHE Claude's avatar
MARCHE Claude committed
41

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
42 43 44 45
\thispagestyle{empty}

\begin{center}

MARCHE Claude's avatar
MARCHE Claude committed
46 47 48 49 50
\rule\textwidth{0.8mm}

\vfill

{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
51 52 53

\vfill

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

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
58
\begin{LARGE}
59
  Version \whyversion{}, February 2011
MARCHE Claude's avatar
MARCHE Claude committed
60
\end{LARGE}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
61 62 63

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
64 65
\begin{Large}
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
66 67 68 69
  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
70 71 72 73 74 75
\end{tabular}
\end{Large}
\vfill

\begin{flushleft}

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

MARCHE Claude's avatar
MARCHE Claude committed
81
\bigskip
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
82

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

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

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
93 94
\chapter*{Foreword}

95 96
This is the manual for the Why platform version 3, or \why\ for
short. \why\ is a complete reimplementation of the former Why
97 98 99 100 101 102 103 104
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\
formalisations or to add support for a new external
prover if wanted.
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
105

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
106
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
107

MARCHE Claude's avatar
MARCHE Claude committed
108 109 110 111
\why\ project page is \url{http://why3.gforge.inria.fr/}.
%\url{https://gforge.inria.fr/projects/why3}.
The last distribution is available, in source format, together with
this documentation and several examples.
MARCHE Claude's avatar
MARCHE Claude committed
112

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

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

There is a public mailing list for users' discussions:
\url{http://lists.gforge.inria.fr/mailman/listinfo/why3-club}.

125
Report any bug to the \why\ Bug Tracking System:
MARCHE Claude's avatar
MARCHE Claude committed
126 127 128
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.


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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
135 136
\subsection*{Summary of Changes w.r.t. Why 2}
The main new features with respect to Why 2.xx
MARCHE Claude's avatar
MARCHE Claude committed
137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 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
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}
  \item concept of proof task 
  \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
  allow access to Why3 features programmatically.

\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
190 191 192 193
\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
194

195
%\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
196

MARCHE Claude's avatar
MARCHE Claude committed
197 198
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
199 200
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
201
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
202

MARCHE Claude's avatar
MARCHE Claude committed
203
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
204

MARCHE Claude's avatar
MARCHE Claude committed
205
% \input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
206

MARCHE Claude's avatar
doc  
MARCHE Claude committed
207 208
\input{api.tex}

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

211
% \input{glossary.tex}
Andrei Paskevich's avatar
Andrei Paskevich committed
212

MARCHE Claude's avatar
MARCHE Claude committed
213 214 215 216
\input{syntaxref.tex}

\input{library.tex}

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

219 220
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
221

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

MARCHE Claude's avatar
MARCHE Claude committed
224
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
225 226
\bibliography{manual}
%\input{biblio-demons}
227

MARCHE Claude's avatar
MARCHE Claude committed
228 229 230

\cleardoublepage
\listoffigures
231 232 233
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
234
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
235 236 237 238 239 240

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