manual.tex 4.21 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
\begin{Large}
  \begin{tabular}{c}
MARCHE Claude's avatar
MARCHE Claude committed
59 60 61 62
  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
63 64 65 66 67 68
\end{tabular}
\end{Large}
\vfill

\begin{flushleft}

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
69
\begin{tabular}{l}
MARCHE Claude's avatar
MARCHE Claude committed
70 71
$^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
72 73
\end{tabular}

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

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

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

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

88 89
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
90 91 92 93
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
94 95
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
96 97


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

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

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

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

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

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


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

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

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

\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
139 140 141
% \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
142
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
143 144 145 146
\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
147

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

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

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

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

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

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

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

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

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

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

\input{library.tex}

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

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

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

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

181 182 183
\cleardoublepage
\printindex

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

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