manual.tex 4.45 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 59 60
\begin{LARGE}
  Version \whyversion{}, December 2010
\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

MARCHE Claude's avatar
MARCHE Claude committed
83
  \textcopyright 2010 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
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
97 98 99 100
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
101 102
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
103 104


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

MARCHE Claude's avatar
MARCHE Claude committed
107 108 109 110
\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
111

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

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

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

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


MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
128
\section*{Acknowledgements}
MARCHE Claude's avatar
MARCHE Claude committed
129

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

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
133
\section*{Release notes}
MARCHE Claude's avatar
MARCHE Claude committed
134 135 136 137 138 139 140 141 142 143 144 145 146

\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
147 148 149
% \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
150
\end{itemize}
MARCHE Claude's avatar
MARCHE Claude committed
151 152 153 154
\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
155

MARCHE Claude's avatar
roadmap  
MARCHE Claude committed
156
\input{intro.tex}
MARCHE Claude's avatar
MARCHE Claude committed
157

MARCHE Claude's avatar
MARCHE Claude committed
158 159
\part{Tutorial}

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

MARCHE Claude's avatar
doc  
MARCHE Claude committed
162
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
163

MARCHE Claude's avatar
MARCHE Claude committed
164
% \input{ide.tex}
MARCHE Claude's avatar
MARCHE Claude committed
165

MARCHE Claude's avatar
MARCHE Claude committed
166
% \input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
167

MARCHE Claude's avatar
doc  
MARCHE Claude committed
168 169
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
170 171
\part{Reference Manual}

172
% \input{glossary.tex}
Andrei Paskevich's avatar
Andrei Paskevich committed
173

MARCHE Claude's avatar
MARCHE Claude committed
174 175 176 177
\input{syntaxref.tex}

\input{library.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
178 179
\input{manpages.tex}

180 181
% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)
MARCHE Claude's avatar
MARCHE Claude committed
182

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

MARCHE Claude's avatar
MARCHE Claude committed
185
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
186 187
\bibliography{manual}
%\input{biblio-demons}
188

189 190 191
\cleardoublepage
\printindex

MARCHE Claude's avatar
MARCHE Claude committed
192
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
193 194 195 196 197 198

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