Commit 89435c10 authored by MARCHE Claude's avatar MARCHE Claude

reorg of manual

parent 22d325ab
...@@ -3,22 +3,29 @@ ...@@ -3,22 +3,29 @@
== Documentation == == Documentation ==
* API: Andrei + Francois 1 Introduction (TODO: a finir)
* tools: IDE (Claude) 2 Syntax, tutorial: JCF + Andrei3
3 IDE (Claude)
4 Standard lib of theories: TODO
* semantics: * semantics:
* tutorial for API: * tutorial for API:
** build a task ** build a task (done)
** call a prover ** call a prover (done)
** apply a transformation ** apply a transformation (TODO)
** develop a new transformation ** develop a new transformation (TODO)
* API: Andrei + Francois
== IDE == == IDE ==
(Claude) (Claude)
* database, session save and restore * database, session save and restore (done)
* Coq output * Coq output (done)
* Gappa output * Gappa output (done)
* debug hide goals (TODO)
* add transf "inline goal" (TODO)
* add button "remove" (TODO)
* add button "replay" (TODO)
== Misc == == Misc ==
...@@ -27,12 +34,12 @@ ...@@ -27,12 +34,12 @@
* LICENSE (done) * LICENSE (done)
* OCAML-LICENSE (TODO: Andrei) * OCAML-LICENSE (TODO: Andrei)
* Builtin arrays in provers (Francois) * Builtin arrays in provers (TODO: Francois)
* make install (done) * make install (done)
* make export (TODO: JCF) * make export (TODO: JCF)
* "make -j" (done) * "make -j" (done)
* META for ocamlfind (TODO: ?) * META for ocamlfind (TODO: Francois)
* headers (TODO: ?) * headers (done)
......
...@@ -232,7 +232,7 @@ constructed. ...@@ -232,7 +232,7 @@ constructed.
Here is the way we build the formula $2+2=4$. The main difficult is to Here is the way we build the formula $2+2=4$. The main difficult is to
access the internal identifier for addition: it must be retrieved from access the internal identifier for addition: it must be retrieved from
the standard theory \texttt{Int} of the file \texttt{int.why} (see the standard theory \texttt{Int} of the file \texttt{int.why} (see
Section~\ref{theory:Int}). Chap~\ref{chap:library}).
\begin{verbatim} \begin{verbatim}
let two : Term.term = Term.t_const (Term.ConstInt "2") let two : Term.term = Term.t_const (Term.ConstInt "2")
let four : Term.term = Term.t_const (Term.ConstInt "4") let four : Term.term = Term.t_const (Term.ConstInt "4")
......
\chapter{IDE} \chapter{Tools}
\label{chap:ide} \label{chap:tools}
\section{Why3 command line tool}
\section{IDE} \section{IDE}
hello \section{Other tools}
\begin{itemize}
\item why-config
\item why-bench
\end{itemize}
%%% Local Variables: %%% Local Variables:
......
...@@ -32,16 +32,20 @@ manuals, giving detailed technical informations. ...@@ -32,16 +32,20 @@ manuals, giving detailed technical informations.
Chapter~\ref{chap:syntax} presents the input syntax for file defining Chapter~\ref{chap:syntax} presents the input syntax for file defining
Why theories. The semantics is given informally with examples. Why theories. The semantics is given informally with examples.
Chapter~\ref{chap:ide} explains how to use the Why IDE for visualizing Chapter~\ref{chap:tools} explains how to use the various command line
theories and goals, call external provers for trying to solve them, tools and the Why IDE for visualizing theories and goals, call
apply transformations to simplify them. The two first chapters are external provers for trying to solve them, apply transformations to
thus to read for the beginners. simplify them. The two first chapters are thus to read for the
beginners.
Chapter~\ref{chap:library} documents the standard library of theories Chapter~\ref{chap:library} documents the standard library of theories
distributed with Why3. Chapter~\ref{chap:whyml} presents the distributed with Why3.
verification condition generator built upon the Why3 core. The two
next chapters are for users with a little more experience, in %Chapter~\ref{chap:whyml} presents the
particular those who wants to use Why for verification of algorithms. %verification condition generator built upon the Why3 core.
% The two
% next chapters are for users with a little more experience, in
% particular those who wants to use Why for verification of algorithms.
Chapter~\ref{chap:api} presents how to use Why3 programmatically, Chapter~\ref{chap:api} presents how to use Why3 programmatically,
using the API. It is for the experimented users, who wants to link using the API. It is for the experimented users, who wants to link
......
\chapter{Standard Library} \chapter{Standard Library}
\label{chap:library} \label{chap:library}
\section{Integers} \begin{description}
\label{theory:Int}
\section{Integer divisions} \item[algebra]
Euclidean versus Computer division \item[int]
\section{Arrays} division: Euclidean versus Computer
\section{Real numbers}
\section{Floating-point numbers} \item[array]
\item[bool]
\item[comparison]
\item[floating\_point]
\cite{ayad10ijcar} \cite{ayad10ijcar}
\item[graph]
\item[list]
\item[option]
\item[real]
\item[relations]
\item[set]
\item[sum]
\end{description}
%%% Local Variables: %%% Local Variables:
%%% mode: latex %%% mode: latex
......
...@@ -76,18 +76,24 @@ We gratefully thank all the people who contributed to this document: ...@@ -76,18 +76,24 @@ We gratefully thank all the people who contributed to this document:
\input{intro.tex} \input{intro.tex}
\part{Tutorial}
\input{syntax.tex} \input{syntax.tex}
\input{ide.tex} \input{ide.tex}
\input{library.tex}
% \input{whyml.tex} % \input{whyml.tex}
\input{api.tex} \input{api.tex}
\part{Reference Manual}
\input{glossary.tex} \input{glossary.tex}
\input{syntaxref.tex}
\input{library.tex}
\input{manpages.tex} \input{manpages.tex}
\chapter{Complete API documentation} \chapter{Complete API documentation}
......
\chapter{Syntax Reference}
\label{chap:syntaxref}
This chapter gives the grammar for the input files
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment