Commit 21175658 authored by MARCHE Claude's avatar MARCHE Claude

doc: more about Why3 command

parent 6c1e5397
......@@ -296,15 +296,19 @@ The second argument of \texttt{f\_close\_quant} is a list of triggers.
\section{Building Theories}
TODO
[TO BE COMPLETED]
\section{Applying transformations}
TODO
[TO BE COMPLETED]
\section{Writing new functions on term}
TODO: pattern-matching on terms, opening a quantifier
[TO BE COMPLETED]
% pattern-matching on terms, opening a quantifier
%%% Local Variables:
%%% mode: latex
......
......@@ -10,7 +10,7 @@
integer ::= digit (digit | "_")* ; decimal
| ("0x" | "0X") hex-digit (hex-digit | "_")* ; hexadecimal
| ("0o" | "0O") oct-digit (oct-digit | "_")* ; octal
| ("0b" | "0B") bin-digit (bin-digit | "_")* ; octal
| ("0b" | "0B") bin-digit (bin-digit | "_")* ; binary
\
real ::= digit+ exponent ; decimal
| digit+ "." digit* exponent? ;
......
......@@ -26,8 +26,7 @@ TODO: continue
\section{Organization of this document}
This document is organized as follows. The first three chapters are
user manuals, to learn how to use Why3. Other chapters are reference
This document is organized as follows. The first part, made of three chapters, provides tutorials to learn how to use Why3. The second part gathers reference
manuals, giving detailed technical informations.
Chapter~\ref{chap:starting} explains how to get started with the Why
......@@ -38,9 +37,6 @@ batch. Chapter~\ref{chap:syntax} presents the input syntax for file
defining Why theories. The semantics is given informally with
examples. The two first chapters are thus to read for the beginners.
Chapter~\ref{chap:library} documents the standard library of theories
distributed with Why3.
%Chapter~\ref{chap:whyml} presents the
%verification condition generator built upon the Why3 core.
% The two
......@@ -51,12 +47,16 @@ Chapter~\ref{chap:api} presents how to use Why3 programmatically,
using the API. It is for the experimented users, who wants to link
Why3 library with their own code.
Chapter~\ref{chap:manpages} are the technical manual pages for the
tools of the platform. All tool options, and all the configuration
files are described in details there.
Chapter~\ref{chap:apidoc} is the technical documentation of the API.
Part 2 provides:
\begin{itemize}
\item In Chapter~\ref{chap:syntaxref}, the input syntax of files.
\item In Chapter~\ref{chap:library}, the standard library of
theories distributed with Why3.
\item In Chapter~\ref{chap:manpages}, the technical manual pages for the
tools of the platform. All tool options, and all the configuration
files are described in details there.
\item In Chapter~\ref{chap:apidoc}, the technical documentation of the API.
\end{itemize}
%%% Local Variables:
......
......@@ -3,10 +3,25 @@
We provide here a short description of logic symbols defined in the
standard library. Only the most general-purpose ones are
described. For more details, one shoudl directly read the
corresponding file.
For each library, we describe the symbols of each theories.
described. For more details, one should directly read the
corresponding file, or alternatively, use the \verb|why3| with option \verb|-T| and a qualified theory name, \eg
\begin{verbatim}
> why3 -T bool.Ite
theory Ite
(* use BuiltIn *)
(* use Bool *)
logic ite (b:bool) (x:'a) (y:'a) : 'a =
match b with
| True -> x
| False -> y
end
end
\end{verbatim}
In the following, for each library, we describe the (main) symbols of
each theories defined
\section{Library bool}
......@@ -32,7 +47,7 @@ For each library, we describe the symbols of each theories.
down, written as \verb|div| and \verb|mod|
\item[ComputerDivision] division and modulo, where division rounds to
zero, alsos written as \verb|div| and \verb|mod|
zero, also written as \verb|div| and \verb|mod|
\item[MinMax] \verb|min| and \verb|max| operators
......
......@@ -91,28 +91,28 @@ of the same prover, or with different options.
The provers which are typically attemped for detection are
\begin{itemize}
\item Alt-Ergo~\cite{conchon08smt,ergo}: \url{}
\item CVC3~\cite{BarTin-CAV-07}: \url{}
\item Coq~\cite{CoqArt}: \url{}
\item Eprover~: \url{}
\item Gappa~\cite{melquiond08rnc}: \url{}
\item Simplify~\cite{simplify05}: \url{}
\item Spass~: \url{}
\item veriT~: \url{}
\item Yices~\cite{DM06}: \url{}
\item Z3~\cite{z3}: \url{}
\item Alt-Ergo~\cite{conchon08smt,ergo}: \url{http://alt-ergo.lri.fr}
\item CVC3~\cite{BarTin-CAV-07}: \url{http://cs.nyu.edu/acsys/cvc3/}
\item Coq~\cite{CoqArt}: \url{http://coq.inria.fr}
\item Eprover~\cite{schulz04ijcar}: \url{http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html}
\item Gappa~\cite{melquiond08rnc}: \url{http://gappa.gforge.inria.fr/}
\item Simplify~\cite{simplify05}: \url{http://secure.ucd.ie/products/opensource/Simplify/}
\item Spass~: \url{http://www.spass-prover.org/}
\item veriT~: \url{http://www.verit-solver.org/}
\item Yices~\cite{DM06}: \url{http://yices.csl.sri.com/}
\item Z3~\cite{z3}: \url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}
\end{itemize}
\texttt{why3config} also detects the plugin installed in the Why3
\texttt{why3config} also detects the plugins installed in the Why3
plugins directory (\eg{} \texttt{/usr/local/lib/why3/plugins}). A
plugin must register itself as a parser, a transformation or a
printer, as explained in the corresponding section.
If the user's configuration file is already present,
\texttt{why3config} will only reset unset variables to default value.
The option \texttt{autodetect-provers} will detect again the available
The option \texttt{--autodetect-provers} will detect again the available
provers and will replace them in the file configuration.
\texttt{autodetect-plugins} will do the same for plugins.
\texttt{--autodetect-plugins} will do the same for plugins.
\section{The \texttt{why3} command-line tool}
\label{sec:why3ref}
......@@ -173,13 +173,25 @@ used to provide other informations :
\item[-I] $d$: adds $d$ in the load path, to search for theories.
\end{description}
\subsection{Left toolbar}
\subsection{Left toolbar actions}
\begin{description}
\item[Context] The context in which the other tools below will
apply. If ``only unproved goals'' is selected, no action will ever
be applied to an already proved goal. If ``all goals'', then
actions are performed even if the goal is already proved. The second
choice allows to compare provers on the same goal.
\item[Provers] To each detected prover corresponds to a button in this
prover framed box. Clicking on this button starts the prover on the
selected goal(s).
\item[Split] This splits the current goal into subgoals if it is a
conjunction of two or more goals.
\item[Inline] If the goal is headed by a defined predicate symbol,
expands it with this definition. [NOT YET AVAILABLE]
\item[Edit] Start an editor on the selected task.
For automatic provers, this allows to see the file sent to the
......@@ -189,23 +201,34 @@ used to provide other informations :
corresponding proof script. The modifications are saved, and can be
retrieved later even if the goal was modified.
\item[Split] This splits the current goal into subgoals if it is a
conjunction of two or more goals.
\item[Replay] replay all obsolete proofs [NOT YET AVAILABLE]
\item[Remove] Remove a proof attempt or a transformation. [NOT YET AVAILABLE]
\end{description}
\subsection{Menus}
\begin{description}
\item[File/Detect provers]
\item[File/Detect provers] runs provers auto-detection
\item[File/Preferences] opens a window for modifying preferred configuration
\end{description}
\subsection{Preferences}
The preferences window allows you customize
\begin{itemize}
\item the default editor to use when the \textsf{Edit} button is
pressed. This might be overidden for a specific prover (the only way
to do that for the moment is to manually edit the config file)
\item the time limit given to provers, in seconds
\item the maximal number of simultaneous provers allowed to run in parallel.
\end{itemize}
\subsection{Structure of the database file}
[TODO]
[TO BE COMPLETED]
\section{The \texttt{why3bench} tool}
......@@ -279,6 +302,7 @@ the keys inside a section matter only for the multi-value key.
The drivers of external provers are
\section{Transformations}
\label{sec:transformations}
\subsection{Non-splitting transformations}
......
......@@ -175,3 +175,15 @@
year = {2007}
}
@InProceedings{schulz04ijcar,
author = {S. Schulz},
title = {{System Description: E~0.81}},
booktitle = {Proc.\ of the 2nd IJCAR, Cork, Ireland},
editor = {D. Basin and M. Rusinowitch},
volume = 3097,
series = {LNAI},
year = 2004,
publisher = {Springer},
pages = {223--228},
}
......@@ -96,7 +96,7 @@ Why3 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} od this document for more detailed
Section~\ref{sec:install} of this document for more detailed
instructions.
\subsection*{Contact}
......
......@@ -44,15 +44,16 @@ The GUI is launched on the file above as follows.
why3ide hello_proof.why
\end{verbatim}
When the GUI is started for the first time, you should get a window
which look like the screenshot of Figure~\ref{fig:gui1}. First of all,
the left row is a tool bar which provide different actions to apply on
goals. In this case, the section ``Provers'' is empty, which means
that you did not perform prover detection yet. You should do it now
using the menu \textsf{File/Detect provers}. Second, the middle part
is a tree view that allows to browse inside the theories. Initially,
the item of this tree are closed. You should now expand this view
using the menu \textsf{View/Expand all} or its shortcut
\textsf{Ctrl-E}. This should result is something like the screenshot of Figure~\ref{fig:gui2}.
which looks like the screenshot of Figure~\ref{fig:gui1}. First of
all, the left row is a tool bar which provide different actions to
apply on goals. In this case, the section ``Provers'' is empty, which
means that you did not perform prover detection yet. You should do it
now using the menu \textsf{File/Detect provers}. Second, the middle
part is a tree view that allows to browse inside the
theories. Initially, the item of this tree are closed. You should now
expand this view using the menu \textsf{View/Expand all} or its
shortcut \textsf{Ctrl-E}. This should result is something like the
screenshot of Figure~\ref{fig:gui2}.
\begin{figure}[tbp]
\includegraphics[width=\textwidth]{gui2.png}
......@@ -92,7 +93,7 @@ get the display of Figure~\ref{fig:gui3}.
The row corresponding to goal $G_1$ is now closed, and marked with
green ``checked'' icon in the status column. This means that the goal
is proved by the Simplify prover. On the contrary, the two other goals
are not proved, they are mark with an orange question mark.
are not proved, they are marked with an orange question mark.
You can immediately attempt to prove the remaining goals using another
prover, {\eg} Alt-Ergo, by clicking on the corresponding button. The
......@@ -104,7 +105,7 @@ Instead of calling a prover on a goal, you can apply a transformation
to it. Since $G_2$ is a conjunction, a possibility is to split it
into subgoals. You can do that by clicking on the \textsf{Split}
button of section ``Transformations'' of the left toolbar. Now you
have two subgoals, and you can try again a prover in them, for example
have two subgoals, and you can try again a prover on them, for example
Simplify. Assuming we expand everything again, you should see now what
is displayed on Figure~\ref{fig:gui4}.
......@@ -116,7 +117,7 @@ is displayed on Figure~\ref{fig:gui4}.
The first part of goal $G_2$ is still unproved. As a last resort, we
can try to call the Coq proof assistant. The first step is to click on
the \textsf{Coq} button. A new sub-row appear for coq, and
the \textsf{Coq} button. A new sub-row appear for Coq, and
unsurprisingly the goal is not proved by Coq either. What can be done
now is editing the proof: select that row and then click on the
\textsf{Edit} button in section ``Tools'' of the toolbar. This should
......@@ -142,7 +143,7 @@ explained below.
\subsection{Modifying the input}
Currently, the GUI does not allow to modify the input file. You must
exit the GUI and modify the file by some editor of your choice. Let's assume we change the goal $G_2$ into
exit the GUI and modify the file by some editor of your choice. Let's assume we change the goal $G_2$ by replacing the first occurrence of true by false, \eg
\begin{verbatim}
goal G2 : (false -> false) and (true or false)
\end{verbatim}
......@@ -163,17 +164,72 @@ shown but marked with "(obsolete)" so that you know the results are
not accurate. You can now retry to prove all what remains unproved
using any of the provers.
\section{Getting Started with the Why3 Command}
\label{sec:batch}
The why3 command allows to check the validity of goals with external
provers, in batch mode. This section presents the basic use of this
tool. Refer to Section~\ref{sec:why3ref} for a more complete
description.
description of this tool and all its command-line options.
The very first time you want to use Why, you should proceed with
autodetection of external provers. This is done as follows, where ``>'' is the prompt.
\begin{verbatim}
> why3config --autodetect-provers
\end{verbatim}
This prints some information messages on what detections are attempted. To know which
provers have been successfully detected, you can run do as follows.
\begin{verbatim}
> why3 --list-provers
Known provers:
alt-ergo (Alt-Ergo)
coq (Coq)
simplify (Simplify)
\end{verbatim}
The first word of each line is a unique identifier for the associated prover. We thus
have now the three provers Alt-Ergo~\cite{ergo}, Coq~\cite{CoqArt} and
Simplify~\cite{simplify05}.
Let's assume now we want to run Simplify on the HelloProof
example. The command to type and its output are as follows, where the
\verb|-P| option is follow by the unique identifier as shown as above.
\begin{verbatim}
> why3 -P simplify hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.10s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.01s)
hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s)
\end{verbatim}
[TO BE COMPLETED]
You can also specify which goal(s) to prove. This is done by giving
first a theory identifier, then goal identifier(s). Here is the way to
call Alt-Ergo on goal $G_2$ and $G_3$.
\begin{verbatim}
> why3 -P alt-ergo hello_proof.why -T HelloProof -G G2 -G G3
hello_proof.why HelloProof G2 : Unknown: Unknown (0.01s)
hello_proof.why HelloProof G3 : Valid (0.01s)
\end{verbatim}
Finally, a transformation to apply to goals before proving them can be
specified. To know the unique identifier associated to transformations, do as follows.
\begin{verbatim}
> why3 --list-transforms
Known non-splitting transformations:
[...]
Known splitting transformations:
[...]
split_goal
split_intro
\end{verbatim}
Here is how you can split the goal $G_2$ before calling
Simplify on resulting subgoals.
\begin{verbatim}
> why3 -P simplify hello_proof.why -a split_goal -T HelloProof -G G2
hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s)
hello_proof.why HelloProof G2 : Valid (0.00s)
\end{verbatim}
Section~\ref{sec:transformations} gives the description of the various
transformations available.
......
......@@ -9,7 +9,8 @@ This chapter gives the grammar for \why\ input files.
Comments are enclosed by \texttt{(*} and \texttt{*)} and can be nested.
\paragraph{Strings.}
Strings are enclosed by double quotes (\verb!"!).
Strings are enclosed by double quotes (\verb!"!). Double quotes can be
inserted in strings using the backslash character (\verb!\!).
% TODO: escape sequences for strings
......
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