Commit ee42e57d authored by MARCHE Claude's avatar MARCHE Claude

roadmap

parent f4a218c2
......@@ -3,31 +3,32 @@
== Documentation ==
1 Introduction (TODO: a finir)
1 Introduction (done: enlevee)
2 getting started (Claude: done, to be read by others)
3 Syntax, tutorial (TODO: JCF + Andrei)
3 Syntax, tutorial (TODO: Andrei)
4 tutorial for API:
** build a task (Claude: done, to be read by others)
** call a prover (Claude: done, to be read by others)
** apply a transformation (TODO ?)
** develop a new transformation (TODO ?)
5 syntax reference (TODO)
6 Standard lib of theories:
** call a prover (Claude: done, to be read by others)
** apply a transformation (a completer plus tard)
** develop a new transformation (a completer plus tard)
5 syntax reference (a completer plus tard par typage et semantique)
6 Standard lib of theories:
(Claude: done, although quite sparse, to be read by others)
7 Manpages
7.1 Compilation, Installation (done)
7.2 external provers (done)
7.3 why3config (TODO Francois)
7.4 why3 (TODO François)
7.5 whyml (TODO ?)
7.6 IDE (TODO, Claude)
7.3 why3config (done)
7.4 why3 (done)
7.5 whyml (done)
7.6 IDE (done)
7.7 whybench (TODO Francois)
7.8 why.conf (TODO Francois)
7.9 drivers (TODO Francois)
7.10 transformations (TODO)
** citation cruanes10 inexistent
7.8 why.conf (done)
7.9 drivers (to be done later)
7.10 transformations (done)
8 API: Andrei + Francois
(should we really add that in the doc ?)
** on remplace par la version HTML a mettre sur la forge INRIA (Francois)
** TODO: mettre un titre au HTML engendré
== IDE ==
......@@ -38,7 +39,7 @@
* Gappa output (done)
* debug hide goals (TODO)
* add "context" options (partially done)
** semantics not clear, should be clarified, documented and
** semantics not clear, should be clarified, documented and
implemented accordingly
* add transf "inline goal" (TODO, not urgent)
* add button "remove"
......@@ -52,14 +53,16 @@
* README (done)
* INSTALL (done)
* LICENSE (done)
* OCAML-LICENSE (TODO: Andrei)
* OCAML-LICENSE (done)
* TODO: licence pour les boomy icons
* option -version a tous les executables (TODO)
* debuguer cpulimit pour gappa (pb de return code)
* option -version a tous les executables (TODO: Andrei)
** + affichage dans l'IDE (done)
* Builtin arrays in provers (TODO: Francois)
* Builtin arrays in provers (done)
* make install (done)
* make export (TODO: JCF)
* make distrib (done)
* "make -j" (done)
* META for ocamlfind (done)
* headers (done)
......
\chapter{The \why\ Application Programming Interface}
\chapter{The \why\ API}
\label{chap:api}
This chapter is a tutorial for the users who wants to link their own
......@@ -76,7 +76,7 @@ Notice that the concrete syntax of \why\ forbids predicate identifiers
to start with a capital letter. This constraint does not exist when
building those directly using library calls.
\section{Buildings Tasks}
\section{Building Tasks}
Let's see how we can call a prover to prove a formula. As said in
previous chapters, a prover must be given a task, so we need to build
......
......@@ -90,7 +90,7 @@ each theories defined
\end{description}
\section{Library floating\_point}
\section{Library \texttt{floating\_point}}
This library provides a theory of IEEE-754 floating-point numbers. It
is inspired from~\cite{ayad10ijcar}.
......@@ -108,7 +108,7 @@ is inspired from~\cite{ayad10ijcar}.
\end{description}
\section{Library Array}
\section{Library \texttt{array}}
\begin{description}
......
......@@ -162,14 +162,16 @@ following steps :
\texttt{-P/--prover} is used.
\end{enumerate}
\texttt{why3} call the prover sequentially, use \texttt{why3bench} if
you want to call the provers concurrently. \why\ can also be
used to provide other informations :
\begin{itemize}
\item \texttt{print-namespace} print the namespace of the selected
theories
\item [TO BE COMPLETED]
\end{itemize}
% \texttt{why3} call the prover sequentially, use \texttt{why3bench} if *)
% you want to call the provers concurrently. *)
% \why\ can also be *)
% used to provide other informations : *)
% \begin{itemize} *)
% \item \texttt{print-namespace} print the namespace of the selected *)
% theories *)
% \item TO BE COMPLETED *)
% \end{itemize} *)
\section{The \texttt{why3ide} GUI}
\label{sec:ideref}
......@@ -318,9 +320,8 @@ the example, or it can be composed by a family name and one family
argument, \texttt{prover} is one family name, \texttt{coq} and
\texttt{alt-ergo} are the family argument.
Inside a section, one key can be associated to an integer (.eg -555),
a boolean (true, false) or a string (.eg "emacs"). One key can appear
a boolean (true, false) or a string (\eg{} "emacs"). One key can appear
only once except if its a multi-value key. The order of apparition of
the keys inside a section matter only for the multi-value key.
......@@ -349,64 +350,86 @@ definitions~\cite{paskevich09rr}
\item[eliminate\_builtin] Suppress definitions of symbols which are
declared as builtin in the driver, i.e. with a ``syntax'' rule.
\item[eliminate\_definition]
\item[eliminate\_definition\_func]
Replaces all function definitions with axioms.
\item[eliminate\_definition\_pred]
Replaces all predicate definitions with axioms.
\item[eliminate\_definition]
Apply both transformations above.
\item[eliminate\_mutual\_recursion]
Replaces mutually recursive definitions with axioms.
\item[eliminate\_recursion]
Replaces all recursive definitions with axioms.
\item[eliminate\_if\_fmla] replaces formulas of the form if f1 then f2
else f3 by an equivalent formula using implications and other
connectives. [TO BE COMPLETED LATER]
\item[eliminate\_if\_term] replaces terms of the form \texttt{if
formula then t2 else t3} by lifting them at the level of formulas.
This may introduce \texttt{if then else } in formulas.
\item[eliminate\_if\_term] replaces terms of the form if formula then
t2 else t3 by lift it at the level of the formula [TO BE COMPLETED
LATER]
\item[eliminate\_if\_fmla] replaces formulas of the form \texttt{if f1 then f2
else f3} by an equivalent formula using implications and other
connectives.
\item[eliminate\_if]
apply both two above transformations
Apply both transformations above.
\item[eliminate\_inductive] replaces inductive predicates by
(incomplete) axiomatic definitions, i.e construction axioms and an
inversion axiom [TO BE COMPLETED LATER]
(incomplete) axiomatic definitions, i.e. construction axioms and
an inversion axiom.
\item[eliminate\_let\_fmla]
Eliminates \texttt{let} by substitution, at the predicate level.
\item[eliminate\_let\_term]
Eliminates \texttt{let} by substitution, at the term level.
\item[eliminate\_let]
apply both two above transformations
Apply both transformations above.
\item[eliminate\_mutual\_recursion]
\item[eliminate\_recursion]
\item[encoding\_decorate\_mono]
\item[encoding\_enumeration]
\item[encoding\_simple2]
% \item[encoding\_decorate\_mono]
% \item[encoding\_enumeration]
\item[encoding\_smt]
Encode polymorphic types into monomorphic type~\cite{conchon08smt}.
\item[encoding\_tptp]
Encode theories into unsorted logic~\cite{cruanes10}.
Encode theories into unsorted logic. %~\cite{cruanes10}.
\item[filter\_trigger]
\item[filter\_trigger\_builtin]
\item[filter\_trigger\_no\_predicate]
\item[hypothesis\_selection]
Filter hypothesis of goals~\cite{cruanes10}.
% \item[filter\_trigger] *)
% \item[filter\_trigger\_builtin] *)
% \item[filter\_trigger\_no\_predicate] *)
% \item[hypothesis\_selection] *)
% Filter hypothesis of goals~\cite{couchot07ftp,cruanes10}. *)
\item[inline\_all]
expands all non-recursive definitions.
\item[inline\_goal] Expands all outermost symbols of the goal that
have a non-recursive definition.
\item[inline\_trivial]
removes definitions of the form
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
\end{verbatim}
when each $e_i$ is either a constant or one of the $x_j$, and
each $x_1$ .. $x_n$ occur at most once in the $e_i$
when each $e_i$ is either a ground term or one of the $x_j$, and
each $x_1$ .. $x_n$ occur at most once in the $e_i$
\item[introduce\_premises] moves antecedents of implications and
universal quantifications of the goal into the premises of the task.
\item[remove\_triggers]
% \item[remove\_triggers] *)
% removes the triggers in all quantifications. *)
\item[simplify\_array]
\item[simplify\_array] Automatically rewrites the task using the lemma
\verb|Select_eq| of theory \verb|array.Array|.
\item[simplify\_formula] reduces trivial equalities $t=t$ to True and
then simplifies propositional structure: removes True, False, ``f
\item[simplify\_formula] reduces trivial equalities $t=t$ to true and
then simplifies propositional structure: removes true, false, ``f
and f'' to ``f'', etc.
\item[simplify\_recursive\_definition] reduces mutually recursive
......@@ -441,27 +464,37 @@ P(t)
in a negative position.
\item[simplify\_trivial\_quantification\_in\_goal]
same as above but applies only in the goal.
\item[split\_premise]
splits conjunctive premises.
\end{description}
\subsection{Splitting transformations}
\begin{description}
\item[right\_split]
\item[simplify\_formula\_and\_task]
\item[full\_split\_all]
composition of \texttt{split\_premise} and \texttt{full\_split\_goal}.
\item[full\_split\_goal] puts the goal in a conjunctive form,
returns the corresponding set of subgoals. The number of subgoals
generated may be exponential in the size of the initial goal.
\item[simplify\_formula\_and\_task] same as \texttt{simplify\_formula}
but also removes the goal if it is equivalent to true.
\item[split\_all]
composition of \texttt{split\_premise} and \texttt{split\_goal}.
\item[split\_goal] if the goal is a conjunction of goals, returns the
corresponding set of subgoals.
\item[split\_goal\_pos\_all]
\item[split\_goal\_pos\_axiom]
\item[split\_goal\_pos\_goal]
\item[split\_goal\_pos\_neg\_all]
\item[split\_goal\_pos\_neg\_axiom]
\item[split\_goal\_pos\_neg\_goal]
corresponding set of subgoals. The number of subgoals generated is linear in
the size of the initial goal.
\item[split\_intro]
when a goal is an implication, moves the antecedents into the premises.
\end{description}
......
......@@ -96,7 +96,7 @@ external prover if wanted. A major new feature is also the ability
to use Why programmatically, via a well-designed API.
\subsection{Availability}
\subsection*{Availability}
\why\ project page is \url{https://gforge.inria.fr/projects/why3}. The
last distribution is available, in source format, together with this
......@@ -109,7 +109,7 @@ See the file \texttt{INSTALL} for quick installation instructions, and
Section~\ref{sec:install} of this document for more detailed
instructions.
\subsection{Contact}
\subsection*{Contact}
There is a public mailing list for users' discussions:
\url{http://lists.gforge.inria.fr/mailman/listinfo/why3-club}.
......@@ -118,12 +118,12 @@ Report any bug to the \why\ Bug Tracking System:
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.
\subsection{Acknowledgements}
\section*{Acknowledgements}
We gratefully thank the people who contributed to \why: Simon Cruanes,
Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.
\subsection{Release notes}
\section*{Release notes}
\paragraph{Version 0.10}
Initial release.
......@@ -137,16 +137,16 @@ Initial release.
\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}.
% \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
\tableofcontents
% \input{intro.tex}
\input{intro.tex}
\part{Tutorial}
......
......@@ -16,7 +16,7 @@ theory TestInt
use import int.Int
goal Test1: 2+2 = 4
goal Test1: 2+2 = 5
goal Test2: forall x:int. x*x >= 0
......
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