manual.tex

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

% rubber: module index

%BEGIN LATEX
\usepackage{comment}
%\usepackage{todonotes}
\newcommand{\ahref}[2]{{#2}}
\excludecomment{htmlonly}
\newenvironment{latexonly}{}{}
%END LATEX

%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{upquote}
%END LATEX

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

\usepackage{listings}
\usepackage{xspace}

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

%HEVEA \newstyle{table.lstframe}{width:100\%;border-width:1px;}

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

% avoid double spacing after '.' and ':' in texttt
%BEGIN LATEX
\makeatletter
\let\ttfamily\relax
\DeclareRobustCommand\ttfamily
   {\not@math@alphabet\ttfamily\mathtt\fontfamily\ttdefault\selectfont\frenchspacing}
\makeatother
%END LATEX

\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{}, June 2018
%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 \& University Paris-Sud, Orsay, F-91405 \\
$^2$ Inria Saclay -- \^Ile-de-France, Palaiseau, F-91120
\end{tabular}

%BEGIN LATEX
\bigskip
%END LATEX

\textcopyright 2010--2018 University Paris-Sud, CNRS, Inria

\urldef{\urlutcat}{\url}{http://frama-c.com/u3cat/}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
\urldef{\urlbware}{\url}{http://bware.lri.fr/}
\urldef{\urlproofinuse}{\url}{http://www.spark-2014.org/proofinuse}
\urldef{\urlcolis}{\url}{http://colis.irif.univ-paris-diderot.fr/}
\urldef{\urlvocal}{\url}{https://vocal.lri.fr/}

This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
  \urlutcat\end{latexonly}) ; the `\ahref{\urlhilite}{Hi-Lite}'
\begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
System@tic competitivity cluster ; the `\ahref{\urlbware}{BWare}'
ANR project (ANR-12-INSE-0010\begin{latexonly},
  \urlbware\end{latexonly}) ; the \ahref{\urlproofinuse}{Joint Laboratory ProofInUse} (ANR-13-LAB3-0007\begin{latexonly}, \urlproofinuse\end{latexonly}) ;
the `\ahref{\urlcolis}{CoLiS}' ANR project (ANR-15-CE25-0001\begin{latexonly},
  \urlcolis\end{latexonly}) ; and the `\ahref{\urlvocal}{VOCaL}' ANR project (ANR-15-CE25-008\begin{latexonly},
  \urlvocal\end{latexonly})
\end{flushleft}
\end{center}

\chapter*{Foreword}
%HEVEA\cutname{foreword.html}

%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 also distributed under the form of an OPAM package and a
Debian package.

\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://gitlab.inria.fr/why3/why3/issues}.


\subsection*{Acknowledgements}

We gratefully thank the people who contributed to \why, directly or
indirectly:
Stefan Berghofer,
Sylvie Boldo,
Martin Clochard,
Simon Cruanes,
Sylvain Dailler,
Cl\'ement Fumex,
L\'eon Gondelman,
David Hauzar,
Daisuke Ishii,
Johannes Kanig,
Mikhail Mandrykin,
David Mentr\'e,
Benjamin Monate,
Kim Nguyen,
Thi-Minh-Tuyen Nguyen,
M\'ario Pereira,
Rapha\"el Rieu-Helft,
Sim\=ao Melo de Sousa,
Asma Tafat,
Piotr Trojanek,
Makarius Wenzel.

\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{exec.tex}

% maintaining library.tex up to date is hopeless
% \input{library.tex}

\input{itp.tex}


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

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

\input{technical.tex}

\part{Appendix}

\appendix

\chapter{Release Notes}
%HEVEA\cutname{changes.html}

\section{Release Notes for version 0.90}

TO DISCUSS:

comment mettre a jour l'example bag ? Parametrer par une egalit'e sur
les elements ?


Attention, ne pas introduire 1 variable par champ complique le boulot des prouveurs

``inline'' ne doit pas inliner Map.set

egalite sur les type algebriques ? engendrees automatiquement ?

\subsection{Syntax Changes}

Logical symbols can no longer be used in non-ghost code;
in particular, there is no polymorphic equality in programs any more,
so equality functions must be declared/defined on a per-type basis
(already done for type \texttt{int} in the standard library). The CHANGES
file contains other potential incompatibility.

\begin{center}
\begin{tabular}{|p{0.45\textwidth}|p{0.45\textwidth}|}
\hline
\textbf{version 0.87} & \textbf{version 0.90} \\
\hline
\texttt{function f ...} & \texttt{let function f ...} if called in
                          programs \\
\hline
\texttt{'L:} & \texttt{label L in} \\
\hline
\texttt{at x 'L} & \texttt{x at L} \\
\hline
\texttt{assert \{ ... (old x) ... \}} & \texttt{assert \{ ... (x at Init) ... \}} \\
\hline
\texttt{\char`\\ x. e} & \texttt{fun x -> e} \\
\hline
\texttt{use HighOrd} & nothing, not needed anymore \\
\hline
\texttt{HighOrd.pred ty} & \texttt{ty -> bool} \\
\hline
\texttt{type t model ...} & \texttt{type t = abstract ...} \\
\hline
\texttt{abstract e ensures \{ Q \}} & \texttt{begin ensures \{ Q \} e end} \\
\hline
\texttt{namespace N} & \texttt{scope N} \\
\hline
\texttt{"attribute"} & \texttt{[@attribute]} \\
\hline
\texttt{meta M prop P} & \texttt{meta M lemma P} or \texttt{meta M axiom P} or \texttt{meta M goal P} \\
\hline
\texttt{loop ... end} & \texttt{while true do ... done} \\
\hline
\texttt{type ... invariant \{ ... self.foo ... \}} & \texttt{type ... invariant \{ ... foo ... \}}\\
\hline
\end{tabular}
\end{center}

\subsection{Model types, abstract types}

explain \texttt{private} and ghost fields, \texttt{abstract mutable},
\texttt{private mutable}

\subsection{Polymorphic Equality}

No polymorphic equality in programs. Consequence : no List.mem in
programs, need for List.mem, List.filter, parameterized with a
predicate.

No default equality on algebraic datatypes

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

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

\bibliographystyle{plain}
\bibliography{manual}
%\bibliography{abbrevs,demons,demons2,demons3,team,crossrefs}


% \cleardoublepage
% \input{glossary.tex}

\cleardoublepage
\listoffigures
\cleardoublepage
\printindex

\end{document}

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