manual.tex 5.96 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
\usepackage{xspace}
MARCHE Claude's avatar
MARCHE Claude committed
10

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

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

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

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

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

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

37 38
\makeindex

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

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

\begin{center}

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

\vfill

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

\vfill

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

\vfill

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

\vfill

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

\begin{flushleft}

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

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

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

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

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

MARCHE Claude's avatar
MARCHE Claude committed
96 97
This is the manual for the Why platform version 3, or \why for
short. \why is a complete reimplementation of the former Why
98 99 100
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
MARCHE Claude's avatar
MARCHE Claude committed
101
well-designed API, allowing to use \why as a software library.
102
An important emphasis is put on modularity and genericity,
MARCHE Claude's avatar
MARCHE Claude committed
103
giving the end user a possibility to easily reuse \why
104
formalizations or to add support for a new external
105
prover if wanted.
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
106

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

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

MARCHE Claude's avatar
MARCHE Claude committed
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}.

MARCHE Claude's avatar
MARCHE Claude committed
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
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
133
Lescuyer, Sim\~ao Melo de Sousa, Guillaume Melquiond, 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
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}
152
  \item concept of proof task
MARCHE Claude's avatar
MARCHE Claude committed
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
  \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

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: