manual.tex 4.23 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
%\usepackage[toc,nonumberlist]{glossaries}
%\makeglossaries
Andrei Paskevich's avatar
Andrei Paskevich committed
18

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
19 20
% for ocamldoc generated pages
\usepackage{ocamldoc}
MARCHE Claude's avatar
MARCHE Claude committed
21 22
\let\tt\ttfamily
\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
23

MARCHE Claude's avatar
MARCHE Claude committed
24 25
\usepackage{ifthen}
\input{./macros.tex}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
26

MARCHE Claude's avatar
MARCHE Claude committed
27 28
\input{./version.tex}

29 30
\makeindex

MARCHE Claude's avatar
MARCHE Claude committed
31
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
32 33
\sloppy
\hbadness=1100
MARCHE Claude's avatar
MARCHE Claude committed
34

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
35 36 37 38
\thispagestyle{empty}

\begin{center}

MARCHE Claude's avatar
MARCHE Claude committed
39 40 41 42 43
\rule\textwidth{0.8mm}

\vfill

{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
44 45 46

\vfill

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

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
51 52 53
\begin{LARGE}
  Version \whyversion{}, December 2010
\end{LARGE}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
54 55 56

\vfill

MARCHE Claude's avatar
MARCHE Claude committed
57 58 59 60 61 62 63 64 65 66 67 68
\begin{Large}
  \begin{tabular}{c}
  Fran\c{c}ois Bobot$^{1}$ \\
  Jean-Christophe Filli\^atre$^{2}$  \\
  Claude March\'e$^{3}$ \\
  Andrei Paskevich$^{1}$
\end{tabular}
\end{Large}
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
69 70 71
\begin{tabular}{l}
$^1$ Univ Paris-Sud, Orsay, F-91405 \\
$^2$ LRI, CNRS, Orsay, F-91405 \\
Andrei Paskevich's avatar
Andrei Paskevich committed
72
$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
73 74
\end{tabular}

MARCHE Claude's avatar
MARCHE Claude committed
75
\bigskip
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
76

MARCHE Claude's avatar
MARCHE Claude committed
77
  \textcopyright 2010 Univ Paris-Sud, CNRS, INRIA
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
78

MARCHE Claude's avatar
MARCHE Claude committed
79
  This work has been partly supported by the `U3CAT' national ANR project
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
80 81 82 83 84 85
  (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
86

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
87 88
\chapter*{Foreword}

89 90
This is the manual for the Why platform version 3, or \why\ for
short. \why\ is a complete reimplementation of the former Why
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
91 92 93 94
platform~\cite{filliatre07cav} for program verification.  The major
change is a completely new design of the architecture for calling
external provers. An important emphasis is put on the genericity,
which allows for the end user to easily add the support for a new
95 96
external prover if wanted.  A major new feature is also the ability
to use Why programmatically, via a well-designed API.
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
97 98


MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
99
\subsection*{Availability}
MARCHE Claude's avatar
MARCHE Claude committed
100

101
\why\ project page is \url{https://gforge.inria.fr/projects/why3}.  The
MARCHE Claude's avatar
MARCHE Claude committed
102 103 104
last distribution is available, in source format, together with this
documentation and several examples.

105
\why\ is distributed as open source and freely available under the
MARCHE Claude's avatar
MARCHE Claude committed
106 107 108
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
109
Section~\ref{sec:install} of this document for more detailed
MARCHE Claude's avatar
MARCHE Claude committed
110 111
instructions.

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
112
\subsection*{Contact}
MARCHE Claude's avatar
MARCHE Claude committed
113 114 115 116

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

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


MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
121
\section*{Acknowledgements}
MARCHE Claude's avatar
MARCHE Claude committed
122

123
We gratefully thank the people who contributed to \why: Simon Cruanes,
MARCHE Claude's avatar
MARCHE Claude committed
124
Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.
MARCHE Claude's avatar
MARCHE Claude committed
125

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
126
\section*{Release notes}
MARCHE Claude's avatar
MARCHE Claude committed
127 128 129 130 131 132 133 134 135 136 137 138 139

\paragraph{Version 0.10}
Initial release. 
\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 goal transformation
\item Generic communication with provers
\item Ocaml Library with documented API
\item New GUI with session save and restore
MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
140 141 142
% \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}. *)
MARCHE Claude's avatar
MARCHE Claude committed
143
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
144 145 146 147
\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
148

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
149
\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
150

MARCHE Claude's avatar
MARCHE Claude committed
151 152
\part{Tutorial}

MARCHE Claude's avatar
MARCHE Claude committed
153 154
\input{starting.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
155
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
156

MARCHE Claude's avatar
MARCHE Claude committed
157
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
158

MARCHE Claude's avatar
MARCHE Claude committed
159
% \input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
160

MARCHE Claude's avatar
doc  
MARCHE Claude committed
161 162
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
163 164
\part{Reference Manual}

165
% \input{glossary.tex}
Andrei Paskevich's avatar
Andrei Paskevich committed
166

MARCHE Claude's avatar
MARCHE Claude committed
167 168 169 170
\input{syntaxref.tex}

\input{library.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
171 172
\input{manpages.tex}

173 174
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
175

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

MARCHE Claude's avatar
MARCHE Claude committed
178
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
179 180
\bibliography{manual}
%\input{biblio-demons}
181

182 183 184
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
185
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
186 187 188 189 190 191

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