manual.tex

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

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

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

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

\newcommand{\why}{\textsf{Why3}}
\newcommand{\eg}{\emph{e.g.}}

\input{./version.tex}

\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 Why3 for
short. Why3 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}

Why3 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.

Why3 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} od 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 Why3 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 Why3: Simon Cruanes,
Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.

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

\end{document}

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