manual.tex

\documentclass[a4paper,11pt,twoside,openright]{memoir}

% rubber: module index

\usepackage[T1]{fontenc}
%\usepackage{url}
\usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
\usepackage{graphicx}

\setulmarginsandblock{30mm}{30mm}{*}
\setlrmarginsandblock{30mm}{30mm}{*}
\setheadfoot{15pt}{38pt}
\checkandfixthelayout


%\usepackage[toc,nonumberlist]{glossaries}
%\makeglossaries

% for ocamldoc generated pages
\usepackage{ocamldoc}
\let\tt\ttfamily
\let\bf\bfseries

\usepackage{ifthen}
\input{./macros.tex}

\input{./version.tex}

\makeindex

\begin{document}
\sloppy
\hbadness=1100

\thispagestyle{empty}

\begin{center}

\rule\textwidth{0.8mm}

\vfill

{\fontsize{40}{40pt}\selectfont\bfseries\sffamily The Why3 platform}

\vfill

\rule\textwidth{0.8mm}

\vfill

\begin{LARGE}
  Version \whyversion{}, December 2010
\end{LARGE}

\vfill

\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}

\begin{tabular}{l}
$^1$ Univ Paris-Sud, Orsay, F-91405 \\
$^2$ LRI, CNRS, Orsay, F-91405 \\
$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
\end{tabular}

\bigskip

  \textcopyright 2010 Univ Paris-Sud, CNRS, INRIA

  This work has been partly supported by the `U3CAT' national ANR project
  (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}

\chapter*{Foreword}

This is the manual for the Why platform version 3, or \why\ for
short. \why\ is a complete reimplementation of the former Why
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
external prover if wanted.  A major new feature is also the ability
to use Why programmatically, via a well-designed API.


\subsection*{Availability}

\why\ project page is \url{https://gforge.inria.fr/projects/why3}.  The
last distribution is available, in source format, together with this
documentation and several examples.

\why\ is distributed as open source and freely available under the
terms of the GNU LGPL 2.1. See the file \texttt{LICENSE}.

See the file \texttt{INSTALL} for quick installation instructions, and
Section~\ref{sec:install} of this document for more detailed
instructions.

\subsection*{Contact}

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

Report any bug to the \why\ Bug Tracking System:
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.


\section*{Acknowledgements}

We gratefully thank the people who contributed to \why: Simon Cruanes,
Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.

\section*{Release notes}

\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
% \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}
\cleardoublepage

\tableofcontents


\input{intro.tex}

\part{Tutorial}

\input{starting.tex}

\input{syntax.tex}

% \input{ide.tex}

% \input{whyml.tex}

\input{api.tex}

\part{Reference Manual}

% \input{glossary.tex}

\input{syntaxref.tex}

\input{library.tex}

\input{manpages.tex}

% \chapter{Complete API documentation} *)
% \label{chap:apidoc} *)

% \input{./apidoc.tex} *)

\bibliographystyle{abbrv}
\bibliography{manual}
%\input{biblio-demons}

\cleardoublepage
\printindex

\end{document}

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