manual.tex

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

% rubber: module index

%HEVEA\@addimagenopt{-pdf}

%BEGIN LATEX
% tells memoir style to number subsections
\setsecnumdepth{subsection}
%END LATEX

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

%BEGIN LATEX
\usepackage{graphicx}
%END LATEX
%HEVEA \newcommand{\includegraphics}[2][2]{\imgsrc{#2}}

\usepackage{listings}
\usepackage{xspace}
\usepackage{hevea}

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

% placement of figures
\renewcommand{\textfraction}{0.01}
\renewcommand{\topfraction}{0.99}
\renewcommand{\bottomfraction}{0.99}
%END LATEX
\setcounter{topnumber}{4}
\setcounter{bottomnumber}{4}
\setcounter{totalnumber}{8}

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

% \usepackage{glossary}
% \makeglossary
% \glossary{name={entry name}, description={entry description}}

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

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

\input{./version.tex}

\makeindex

%HEVEA\title{The Why3 platform}

\begin{document}
\sloppy
%BEGIN LATEX
\hbadness=5000
%END LATEX

\thispagestyle{empty}

\begin{center}

%BEGIN LATEX
\rule\textwidth{0.8mm}
%END LATEX

\vfill

{
%BEGIN LATEX
\fontsize{40}{40pt}\selectfont
%END LATEX
%HEVEA \Huge
\bfseries\sffamily The Why3 platform}

\vfill

%BEGIN LATEX
\rule\textwidth{0.8mm}
%END LATEX

\vfill

\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}

%BEGIN LATEX
\begin{LARGE}
%END LATEX
  Version \whyversion{}, October 2012
%BEGIN LATEX
\end{LARGE}
%END LATEX

\vfill

%BEGIN LATEX
\begin{Large}
%END LATEX
  \begin{tabular}{c}
  Fran\c{c}ois Bobot$^{1,2}$ \\
  Jean-Christophe Filli\^atre$^{1,2}$  \\
  Claude March\'e$^{2,1}$ \\
  Guillaume Melquiond$^{2,1}$\\
  Andrei Paskevich$^{1,2}$
\end{tabular}
%BEGIN LATEX
\end{Large}
%END LATEX
\vfill

\begin{flushleft}

\begin{tabular}{l}
$^1$ LRI, CNRS, Univ Paris-Sud, Orsay, F-91405 \\
$^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
\end{tabular}

%BEGIN LATEX
\bigskip
%END LATEX

  \textcopyright 2010-2012 Univ Paris-Sud, CNRS, Inria

\urldef{\urlutcat}{\url}{http://frama-c.cea.fr/u3cat}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}

  This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
  national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
  \urlutcat\end{latexonly}) and by the `\ahref{\urlhilite}{Hi-Lite}'
  \begin{latexonly}(\urlhilite)\end{latexonly} 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 platform for deductive program verification. It provides
a rich language for specification and programming, called \whyml, and
relies on external theorem provers, both automated and interactive,
to discharge verification conditions. \why comes with a standard
library of logical theories (integer and real arithmetic, Boolean
operations, sets and maps, etc.) and basic programming data structures
(arrays, queues, hash tables, etc.). A user can write \whyml programs
directly and get correct-by-construction OCaml programs through an
automated extraction mechanism. \whyml is also used as an intermediate
language for the verification of C, Java, or Ada programs.

\why is a complete reimplementation %~\cite{boogie11why3}
of the former Why platform~\cite{filliatre07cav}.
%for program verification.
Among the new features are: numerous
extensions to the input language, a new architecture for calling
external provers, and a well-designed API, allowing to use \why as a
software library.  An important emphasis is put on modularity and
genericity, giving the end user a possibility to easily reuse \why
formalizations or to add support for a new external prover if wanted.

\subsection*{Availability}

\why project page is \url{http://why3.lri.fr/}.  The last distribution
is available there, 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}.


\subsection*{Acknowledgements}

We gratefully thank the people who contributed to \why, directly or
indirectly: Romain Bardou, Simon Cruanes, Leon Gondelman, Johannes Kanig,
St\'ephane Lescuyer, Sim\~ao Melo de Sousa, Benjamin Monate, Asma Tafat.

\subsection*{Release Notes for version 0.80: syntax changes w.r.t. 0.73}

The syntax of \whyml programs changed in release 0.80. 
The table in Figure~\ref{fig:syntax080} summarizes the changes.

\begin{figure}[t]
  \centering
\begin{tabular}{|l|l|}
\hline
\textbf{version 0.73} & \textbf{version 0.80} \\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
type t = \{| field~:~int |\} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
type t = \{ field~:~int \} \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
\hspace*{3ex} \{| field = 5 |\} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
\hspace*{3ex} \{ field = 5 \} \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
use import module M \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
use import M \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
let rec f (x:int) (y:int)~:~t 
\hspace*{3ex} variant \{ t \} with rel = \\
\hspace*{3ex} \{ P \} \\
\hspace*{3ex} e \\
\hspace*{3ex} \{ Q \} \\
\hspace*{3ex} | Exc1 -> \{ R1 \} \\
\hspace*{3ex} | Exc2 n -> \{ R2 \} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
let rec f (x:int) (y:int)~:~t \\
\hspace*{3ex} variant \{ t with rel \}
\hspace*{3ex} requires \{ P \} \\
\hspace*{3ex} ensures \{ Q \} \\
\hspace*{3ex} raises \{ Exc1 -> R1 \\
\hspace*{3ex}~~~~~~~~| Exc2 n -> R2 \} \\
\hspace*{3ex} = e \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
val f (x:int) (y:int)~:\\
\hspace*{3ex} \{ P \} \\
\hspace*{3ex} t \\
\hspace*{3ex} writes a b \\
\hspace*{3ex} \{ Q \} \\
\hspace*{3ex} | Exc1 -> \{ R1 \} \\
\hspace*{3ex} | Exc2 n -> \{ R2 \} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
val f (x:int) (y:int)~:~t \\
\hspace*{3ex} requires \{ P \} \\
\hspace*{3ex} writes \{ a, b \} \\
\hspace*{3ex} ensures \{ Q \} \\
\hspace*{3ex} raises \{ Exc1 -> R1 \\
\hspace*{3ex}~~~~~~~~| Exc2 n -> R2 \} \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
val f~:~x:int -> y:int ->\\
\hspace*{3ex} \{ P \} \\
\hspace*{3ex} t \\
\hspace*{3ex} writes a b \\
\hspace*{3ex} \{ Q \} \\
\hspace*{3ex} | Exc1 -> \{ R1 \} \\
\hspace*{3ex} | Exc2 n -> \{ R2 \} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
val f (x y:int)~:~t \\
\hspace*{3ex} requires \{ P \} \\
\hspace*{3ex} writes \{ a, b \} \\
\hspace*{3ex} ensures \{ Q \} \\
\hspace*{3ex} raises \{ Exc1 -> R1 \\
\hspace*{3ex}~~~~~~~~| Exc2 n -> R2 \} \\
\end{minipage}
\\
\hline
\begin{minipage}[t]{0.45\textwidth}\ttfamily
abstract e \{ Q \} \\
\end{minipage}
&
\begin{minipage}[t]{0.45\textwidth}\ttfamily
abstract e ensures \{ Q \} \\
\end{minipage}
\\
\hline
\end{tabular}
\caption{Syntax changes from version 0.73 to version 0.80}
\label{fig:syntax080}
\end{figure}

\subsection*{Summary of Changes w.r.t. Why 2}

The main new features with respect to Why 2.xx
are the following.
\begin{enumerate}
\item Completely redesigned input syntax for logic declarations
  \begin{itemize}
  \item new syntax for terms and formulas
  \item enumerated and algebraic data types, pattern matching
  \item recursive definitions of logic functions and predicates, with
    termination checking
  \item inductive definitions of predicates
  \item declarations are structured in components called ``theories'',
    which can be reused and instantiated
  \end{itemize}

\item More generic handling of goals and lemmas to prove
  \begin{itemize}
  \item concept of proof task
  \item generic concept of task transformation
  \item generic approach for communicating with external provers
  \end{itemize}

\item Source code organized as a library with a documented API, to
  allow access to \why features programmatically.

\item GUI with new features with respect to the former GWhy
  \begin{itemize}
  \item session save and restore
  \item prover calls in parallel
  \item splitting, and more generally applying task transformations,
    on demand
  \item ability to edit proofs for interactive provers (Coq only for
    the moment) on any subtask
  \end{itemize}

\item Extensible architecture via plugins
  \begin{itemize}
  \item users can define new transformations
  \item users can add connections to additional provers
  \end{itemize}
\end{enumerate}

% \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 proof task 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

%BEGIN LATEX
\tableofcontents
%END LATEX

%\input{intro.tex}

\part{Tutorial}

\input{starting.tex}

\input{syntax.tex}

% \input{ide.tex}

\input{whyml.tex}

\input{api.tex}

\part{Reference Manual}

\input{install.tex}

\input{manpages.tex}

\input{syntaxref.tex}

\input{library.tex}

\input{realizations.tex}

\input{coq_tactic.tex}

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

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

% \appendix

\input{technical.tex}

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


% \cleardoublepage
% \input{glossary.tex}

\cleardoublepage
\listoffigures
\cleardoublepage
\printindex

\end{document}

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