manual.tex 2.26 KB
Newer Older
1
\documentclass[a4paper,11pt,twoside,openright]{memoir}
MARCHE Claude's avatar
MARCHE Claude committed
2

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
3
\usepackage[T1]{fontenc}
4 5
%\usepackage{url}
\usepackage[a4paper,pdftex,colorlinks=true,urlcolor=blue,pdfstartview=FitH]{hyperref}
MARCHE Claude's avatar
MARCHE Claude committed
6

7 8
%\usepackage[toc,nonumberlist]{glossaries}
%\makeglossaries
Andrei Paskevich's avatar
Andrei Paskevich committed
9

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
10 11
% for ocamldoc generated pages
\usepackage{ocamldoc}
MARCHE Claude's avatar
MARCHE Claude committed
12 13
\let\tt\ttfamily
\let\bf\bfseries
MARCHE Claude's avatar
MARCHE Claude committed
14

15 16
\newcommand{\why}{\textsf{Why3}}
\newcommand{\eg}{\emph{e.g.}}
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
17

MARCHE Claude's avatar
MARCHE Claude committed
18
\begin{document}
MARCHE Claude's avatar
MARCHE Claude committed
19 20
\sloppy
\hbadness=1100
MARCHE Claude's avatar
MARCHE Claude committed
21

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
22 23 24 25 26 27 28 29 30 31 32 33
\thispagestyle{empty}

\begin{center}

~

\vfill

{\Huge\bfseries Why3 manual}

\vfill

Andrei Paskevich's avatar
Andrei Paskevich committed
34 35 36
{\Large F. Bobot$^{1,2}$ \\
J.-C. Filli\^atre$^{2,1}$  \\
C. March\'e$^{3,1}$ \\
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
37 38 39 40 41 42 43
A. Paskevich$^{1,2}$}

\vfill

\begin{tabular}{l}
$^1$ Univ Paris-Sud, Orsay, F-91405 \\
$^2$ LRI, CNRS, Orsay, F-91405 \\
Andrei Paskevich's avatar
Andrei Paskevich committed
44
$^3$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
MARCHE Claude's avatar
biblio  
MARCHE Claude committed
45 46 47 48 49 50 51 52 53 54 55 56 57 58
\end{tabular}

\vfill

\begin{flushleft}
  \textcopyright 2010-2010 Univ Paris-Sud, CNRS, INRIA

  This work has been 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}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
59 60 61 62 63

\cleardoublepage

\tableofcontents

MARCHE Claude's avatar
biblio  
MARCHE Claude committed
64 65 66 67 68 69 70 71
\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
72 73
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
74 75 76 77 78

\section*{Acknowledgements}

We gratefully thank all the people who contributed to this document:

MARCHE Claude's avatar
MARCHE Claude committed
79 80
\input{intro.tex}

MARCHE Claude's avatar
MARCHE Claude committed
81 82
\part{Tutorial}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
83
\input{syntax.tex}
MARCHE Claude's avatar
MARCHE Claude committed
84 85 86

\input{ide.tex}

MARCHE Claude's avatar
MARCHE Claude committed
87
% \input{whyml.tex}
MARCHE Claude's avatar
docs  
MARCHE Claude committed
88

MARCHE Claude's avatar
doc  
MARCHE Claude committed
89 90
\input{api.tex}

MARCHE Claude's avatar
MARCHE Claude committed
91 92
\part{Reference Manual}

93
% \input{glossary.tex}
Andrei Paskevich's avatar
Andrei Paskevich committed
94

MARCHE Claude's avatar
MARCHE Claude committed
95 96 97 98
\input{syntaxref.tex}

\input{library.tex}

MARCHE Claude's avatar
doc  
MARCHE Claude committed
99 100
\input{manpages.tex}

MARCHE Claude's avatar
MARCHE Claude committed
101
\chapter{Complete API documentation}
MARCHE Claude's avatar
MARCHE Claude committed
102
\label{chap:apidoc}
MARCHE Claude's avatar
MARCHE Claude committed
103 104 105

\input{./apidoc.tex}

MARCHE Claude's avatar
MARCHE Claude committed
106
\bibliographystyle{abbrv}
MARCHE Claude's avatar
claude  
MARCHE Claude committed
107 108
\bibliography{manual}
%\input{biblio-demons}
109

MARCHE Claude's avatar
MARCHE Claude committed
110
\end{document}
MARCHE Claude's avatar
doc  
MARCHE Claude committed
111 112 113 114 115 116

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