Commit c64c50c6 authored by Andrei Paskevich's avatar Andrei Paskevich

a lot of minor fixed (to be continued)

parent 01fd5b42
\chapter{The \why\ API}
\label{chap:api}
This chapter is a tutorial for the users who wants to link their own
This chapter is a tutorial for the users who want to link their own
OCaml code with the \why\ library. We progressively introduce the way
one can use the library to build terms, formulas, theories, proof
tasks, call external provers on tasks, and apply transformations on
tasks. The complete documentation for API calls is given
tasks. The complete documentation for API calls is given
[TODO in Chapter~ref{chap:apidoc}.]
We assume the reader has a fair knowledge of the OCaml
language. Notice also that the \why\ library is installed: see
Section~\ref{sec:installlib}.
language. Notice that the \why\ library must be installed,
see Section~\ref{sec:installlib}.
\section{Building Propositional Formulas}
......@@ -53,17 +53,17 @@ Let's now build a formula with propositional variables: $A \land B
\rightarrow A$. Propositional variables must be declared first before
using them in formulas. This is done as follows.
\begin{verbatim}
let prop_var_A : Term.lsymbol =
let prop_var_A : Term.lsymbol =
Term.create_psymbol (Ident.id_fresh "A") []
let prop_var_B : Term.lsymbol =
let prop_var_B : Term.lsymbol =
Term.create_psymbol (Ident.id_fresh "B") []
\end{verbatim}
The type \texttt{lsymbol} is the type of logic symbols. The atoms $A$ and $B$
The type \texttt{lsymbol} is the type of logic symbols. Then the atoms $A$ and $B$
must be built by the general function for applying a predicate symbol to a list of terms. Here we just need the empty list of arguments.
\begin{verbatim}
let atom_A : Term.fmla = Term.f_app prop_var_A []
let atom_B : Term.fmla = Term.f_app prop_var_B []
let fmla2 : Term.fmla =
let fmla2 : Term.fmla =
Term.f_implies (Term.f_and atom_A atom_B) atom_A
let () = printf "@[formula 2 is:@ %a@]@." Pretty.print_fmla fmla2
\end{verbatim}
......@@ -82,37 +82,40 @@ 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
tasks from our formulas. Task can be build incrementally from an empty
task by adding declaration to it, using the functions
\texttt{add\_*\_decl} of module \texttt{Task}. For the formula $true and
\texttt{add\_*\_decl} of module \texttt{Task}. For the formula $true \lor
false$ above, this is done as follows.
\begin{verbatim}
let task1 : Task.task = None (* empty task *)
let goal_id1 : Decl.prsymbol =
Decl.create_prsymbol (Ident.id_fresh "goal1")
let task1 : Task.task =
let goal_id1 : Decl.prsymbol =
Decl.create_prsymbol (Ident.id_fresh "goal1")
let task1 : Task.task =
Task.add_prop_decl task1 Decl.Pgoal goal_id1 fmla1
\end{verbatim}
To make the formula a goal, we must give a name to it, here "goal1". A
goal name has type \texttt{prsymbol}, for identifiers denoting
propositions in a theory or a task. Notice again that the concrete
syntax of \why\ requires these symbol to be capitalized, but it is not
syntax of \why\ requires these symbols to be capitalized, but it is not
mandatory when using the library. The second argument of
\texttt{add\_prop\_decl} is the kind of the proposition:
\texttt{Paxiom}, \texttt{Plemma} or \texttt{Pgoal}.
\texttt{Paxiom}, \texttt{Plemma} or \texttt{Pgoal}
(notice, however, that lemmas are not allowed in tasks
and can only be used in theories).
Once such a task is built, it can be printed.
Once a task is built, it can be printed.
\begin{verbatim}
(* printing the task *)
let () = printf "@[task 1 is:@\n%a@]@." Pretty.print_task task1
\end{verbatim}
The task for our second formula is a bit more complex to build, because the variables A and B must be add as logic declaration in the task.
The task for our second formula is a bit more complex to build, because
the variables A and B must be added as logic declarations in the task.
\begin{verbatim}
(* task for formula 2 *)
let task2 = None
let task2 = Task.add_logic_decl task2 [prop_var_A, None]
let task2 = Task.add_logic_decl task2 [prop_var_B, None]
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
let task2 = Task.add_logic_decl task2 [prop_var_A, None]
let task2 = Task.add_logic_decl task2 [prop_var_B, None]
let goal_id2 = Decl.create_prsymbol (Ident.id_fresh "goal2")
let task2 = Task.add_prop_decl task2 Decl.Pgoal goal_id2 fmla2
let () = printf "@[task 2 is:@\n%a@]@." Pretty.print_task task2
\end{verbatim}
......@@ -129,9 +132,9 @@ end
task 2 is:
theory Task
logic A
logic B
goal Goal2 : A and B -> A
end
\end{verbatim}
......@@ -139,7 +142,7 @@ end
\section{Calling External Provers}
To call an external prover, we need to access the Why configuration
file \texttt{.whyrc}, as it was build using the \texttt{why3config}
file \texttt{why.conf}, as it was build using the \texttt{why3config}
command line tool or the \textsf{Detect Provers} menu of the graphical
IDE. The following API calls allow to access the content of this
configuration file.
......@@ -149,7 +152,7 @@ let config : Whyconf.config = Whyconf.read_config None
(* the [main] section of the config file *)
let main : Whyconf.main = Whyconf.get_main config
(* all the provers detected, from the config file *)
let provers : Whyconf.config_prover Util.Mstr.t =
let provers : Whyconf.config_prover Util.Mstr.t =
Whyconf.get_provers config
\end{verbatim}
The type \texttt{'a Util.Mstr.t} is a map indexed by strings. This map
......@@ -158,9 +161,9 @@ attempt to access the prover Alt-Ergo, which is known to be identified
with id \texttt{"alt-ergo"}.
\begin{verbatim}
(* the [prover alt-ergo] section of the config file *)
let alt_ergo : Whyconf.config_prover =
let alt_ergo : Whyconf.config_prover =
try
Util.Mstr.find "alt-ergo" provers
Util.Mstr.find "alt-ergo" provers
with Not_found ->
eprintf "Prover alt-ergo not installed or not configured@.";
exit 0
......@@ -171,63 +174,64 @@ driver typically depends on the standard theories so these should be
loaded first.
\begin{verbatim}
(* builds the environment from the [loadpath] *)
let env : Env.env =
Env.create_env (Lexer.retrieve (Whyconf.loadpath main))
let env : Env.env =
Env.create_env (Lexer.retrieve (Whyconf.loadpath main))
(* loading the Alt-Ergo driver *)
let alt_ergo_driver : Driver.driver =
let alt_ergo_driver : Driver.driver =
Driver.load_driver env alt_ergo.Whyconf.driver
\end{verbatim}
We are now ready to call the prover on the tasks. This is done by a
function call that launches the external executable and waits for its
termination. Here is a simple way to proceed
termination. Here is a simple way to proceed:
\begin{verbatim}
(* call Alt-Ergo *)
let result1 : Call_provers.prover_result =
(* calls Alt-Ergo *)
let result1 : Call_provers.prover_result =
Driver.prove_task ~command:alt_ergo.Whyconf.command
alt_ergo_driver task1 () ()
(* prints Alt-Ergo answer *)
let () = printf "@[On task 1, alt-ergo answers %a@."
let () = printf "@[On task 1, alt-ergo answers %a@]@."
Call_provers.print_prover_result result1
\end{verbatim}
This way to call a prover is in general to naive, since it may never
This way to call a prover is in general too naive, since it may never
return if the prover runs without time limit. The function
\texttt{prove\_task} has two optional parameters: \texttt{timelimit}
is the maximum allowed running time in seconds, and \texttt{memlimit}
is the maximum allowed memory in megabytes. The type
\texttt{prover\_result} is a record with three fields:
\begin{itemize}
\item \texttt{pr\_answer}: the prover answer, detailed below.
\item \texttt{pr\_answer}: the prover answer, explained below;
\item \texttt{pr\_output}: the output of the prover, i.e. both
standard output and the standard error of the process
\item \texttt{pr\_time} : the time taken by the prover, in seconds
(a redirection in \texttt{why.conf} is required);
\item \texttt{pr\_time} : the time taken by the prover, in seconds.
\end{itemize}
a \texttt{pr\_answer} is a sum of several kind of answers:
A \texttt{pr\_answer} is a sum of several kind of answers:
\begin{itemize}
\item \texttt{Valid}: the task is valid according to the prover.
\item \texttt{Invalid}: the task is invalid.
\item \texttt{Timeout}: the task timeouts, i.e. it takes more time
than specified.
\item \texttt{Timeout}: the prover exceeds the time or memory limit.
\item \texttt{Unknown} $msg$: the prover can't determine if the task
is valid. the string parameter $msg$ indicates some extra
is valid; the string parameter $msg$ indicates some extra
information.
\item \texttt{Failure} $msg$: the prover reports a failure, i.e. it
\item \texttt{Failure} $msg$: the prover reports a failure, i.e.~it
was unable to read correctly its input task.
\item \texttt{HighFailure}: an error occurred while trying to call the
prover, or the prover answer was not understood (i.e. none of the
given regexps in the driver file match the output of the prover).
prover, or the prover answer was not understood (i.e.~none of the
given regular expressions in the driver file matches the output
of the prover).
\end{itemize}
Here is thus another way of calling the Alt-Ergo prover, on our second
task.
\begin{verbatim}
let result2 : Call_provers.prover_result =
let result2 : Call_provers.prover_result =
Driver.prove_task ~command:alt_ergo.Whyconf.command
~timelimit:10
alt_ergo_driver task2 () ()
let () =
let () =
printf "@[On task 2, alt-ergo answers %a in %5.2f seconds@."
Call_provers.print_prover_answer
Call_provers.print_prover_answer
result1.Call_provers.pr_answer
result1.Call_provers.pr_time
\end{verbatim}
......@@ -243,19 +247,19 @@ An important feature of the functions for building terms and formulas
is that they statically guarantee that only well-typed terms can be
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 difficulty is to
access the internal identifier for addition: it must be retrieved from
the standard theory \texttt{Int} of the file \texttt{int.why} (see
Chap~\ref{chap:library}).
\begin{verbatim}
let two : Term.term = Term.t_const (Term.ConstInt "2")
let four : Term.term = Term.t_const (Term.ConstInt "4")
let int_theory : Theory.theory =
let int_theory : Theory.theory =
Env.find_theory env ["int"] "Int"
let plus_symbol : Term.lsymbol =
let plus_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix +"]
let two_plus_two : Term.term =
Term.t_app_infer plus_symbol [two;two]
let two_plus_two : Term.term =
Term.t_app_infer plus_symbol [two;two]
let fmla3 : Term.fmla = Term.f_equ two_plus_two four
\end{verbatim}
An important point to notice as that when building the application of
......@@ -263,51 +267,56 @@ $+$ to the arguments, it is checked that the types are correct. Indeed
the constructor \texttt{t\_app\_infer} infers the type of the resulting
term. One could also provide the expected type as follows.
\begin{verbatim}
let two_plus_two : Term.term =
let two_plus_two : Term.term =
Term.t_app plus_symbol [two;two] Ty.ty_int
\end{verbatim}
When building a task with this formula, we need to declare that we use the Int theory, as follows.
When building a task with this formula, we need to declare that we use
theory \texttt{Int}:
\begin{verbatim}
let task3 = None
let task3 = Task.use_export task3 int_theory
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
let goal_id3 = Decl.create_prsymbol (Ident.id_fresh "goal3")
let task3 = Task.add_prop_decl task3 Decl.Pgoal goal_id3 fmla3
\end{verbatim}
\section{Building Quantified Formulas}
To illustrate how to build quantified formulas, let's build $\forall x:int. x*x \geq 0$. The first step is to obtain the symbols from the int theory.
To illustrate how to build quantified formulas, let us consider
the formula $\forall x:int. x*x \geq 0$. The first step is to
obtain the symbols from \texttt{Int}.
\begin{verbatim}
let zero : Term.term = Term.t_const (Term.ConstInt "0")
let mult_symbol : Term.lsymbol =
let mult_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix *"]
let ge_symbol : Term.lsymbol =
let ge_symbol : Term.lsymbol =
Theory.ns_find_ls int_theory.Theory.th_export ["infix >="]
\end{verbatim}
The next step is to introduce the variable $x$ with the type int.
\begin{verbatim}
let var_x : Term.vsymbol =
let var_x : Term.vsymbol =
Term.create_vsymbol (Ident.id_fresh "x") Ty.ty_int
\end{verbatim}
The formula $x*x \geq 0$ is obtained similarly as the previous example.
The formula $x*x \geq 0$ is obtained as in the previous example.
\begin{verbatim}
let x : Term.term = Term.t_var var_x
let x_times_x : Term.term =
Term.t_app_infer mult_symbol [x;x]
let fmla4_aux : Term.fmla =
Term.f_app ge_symbol [x_times_x;zero]
let x_times_x : Term.term = Term.t_app_infer mult_symbol [x;x]
let fmla4_aux : Term.fmla = Term.f_app ge_symbol [x_times_x;zero]
\end{verbatim}
To quantify on $x$, it is mandatory to first build an intermediate
value of type \texttt{fmla\_quant}.
To quantify on $x$, one can first build an intermediate
value of type \texttt{fmla\_quant}, representing a closure
under a quantifier:
\begin{verbatim}
let fmla4_quant : Term.fmla_quant =
Term.f_close_quant [var_x] [] fmla4_aux
let fmla4 : Term.fmla =
Term.f_forall fmla4_quant
let fmla4_quant : Term.fmla_quant = Term.f_close_quant [var_x] [] fmla4_aux
let fmla4 : Term.fmla = Term.f_forall fmla4_quant
\end{verbatim}
The second argument of \texttt{f\_close\_quant} is a list of triggers.
A simpler method would be to use an appropriate function:
\begin{verbatim}
let fmla4bis : Term.fmla = Term.f_forall_close [var_x] [] fmla4_aux
\end{verbatim}
\section{Building Theories}
[TO BE COMPLETED]
......
......@@ -20,17 +20,17 @@ theory Ite
end
\end{verbatim}
In the following, for each library, we describe the (main) symbols of
each theories defined
In the following, for each library, we describe the (main) symbols
defined in it.
\section{Library \texttt{bool}}
\begin{description}
\item[Bool] boolean data type \verb|bool| with constructors \verb|True| and
\verb|False| ; operations \verb|andb|, \verb|orb|, \verb|xorb|, \verb|notb|
\verb|False|; operations \verb|andb|, \verb|orb|, \verb|xorb|, \verb|notb|.
\item[Ite] polymorphic if-then-else operator written as \verb|ite|
\item[Ite] polymorphic if-then-else operator written as \verb|ite|.
\end{description}
......@@ -38,18 +38,18 @@ each theories defined
\begin{description}
\item[Int] basic operations \verb|+|, \verb|-| and \verb|*| ; comparison
\item[Int] basic operations \verb|+|, \verb|-| and \verb|*|; comparison
operators \verb|<|, \verb|>|, \verb|>=| and \verb|<=|.
\item[Abs] absolute value written as \verb|abs|
\item[Abs] absolute value written as \verb|abs|.
\item[EuclideanDivision] division and modulo, where division rounds
down, written as \verb|div| and \verb|mod|
down, written as \verb|div| and \verb|mod|.
\item[ComputerDivision] division and modulo, where division rounds to
zero, also written as \verb|div| and \verb|mod|
zero, also written as \verb|div| and \verb|mod|.
\item[MinMax] \verb|min| and \verb|max| operators
\item[MinMax] \verb|min| and \verb|max| operators.
\end{description}
......@@ -57,26 +57,26 @@ each theories defined
\begin{description}
\item[Real] basic operations \verb|+|, \verb|-|, \verb|*| and \verb|/| ;
comparison operators
\item[Real] basic operations \verb|+|, \verb|-|, \verb|*| and \verb|/|;
comparison operators.
\item[RealInfix] basic operations with alternative syntax \verb|+.|,
\verb|-.|, \verb|*.|, \verb|/.|, \verb|<.|, \verb|>.|, \verb|<=.| and \verb|>=.|, to
allow a simultaneous use of integer and real operators.
allow simultaneous use of integer and real operators.
\item[Abs] absolute value written as \verb|abs|
\item[Abs] absolute value written as \verb|abs|.
\item[MinMax] \verb|min| and \verb|max| operators
\item[MinMax] \verb|min| and \verb|max| operators.
\item[FromInt] operator \verb|from_int| to convert an integer to a real.
\item[Truncate] conversion operators from real to integers:
\verb|truncate| rounds to 0, \verb|floor| rounds down and
\verb|ceil| rounds up
\verb|ceil| rounds up.
\item[Square] operators \verb|sqr| and \verb|sqrt| for square and square root
\item[Square] operators \verb|sqr| and \verb|sqrt| for square and square root.
\item[ExpLog] functions \verb|exp|, \verb|log|, \verb|log2|, and \verb|log10|
\item[ExpLog] functions \verb|exp|, \verb|log|, \verb|log2|, and \verb|log10|.
\item[Power] function \verb|pow| with two real parameters.
......@@ -93,18 +93,18 @@ each theories defined
\section{Library \texttt{floating\_point}}
This library provides a theory of IEEE-754 floating-point numbers. It
is inspired from~\cite{ayad10ijcar}.
is inspired by~\cite{ayad10ijcar}.
\begin{description}
\item[Rounding] type \verb|mode| with 5 constants
\verb|NearestTiesToEven|, \verb|ToZero|, \verb|Up|, \verb|Down| and
\verb|NearTiesToAway|.
\item[SpecialValues] handling of infinities and NaN
\item[SpecialValues] handling of infinities and NaN.
\item[GenFloat] generic floats parameterized by the maximal
representable number. Functions \verb|round|, \verb|value|,
\verb|exact|, \verb|model|, predicate \verb|no_overflow|.
\item[Single] instance of GenFloat for 32-bits single precision numbers
\item[Double] instance of GenFloat for 64-bits double precision numbers
\item[Single] instance of GenFloat for 32-bits single precision numbers.
\item[Double] instance of GenFloat for 64-bits double precision numbers.
\end{description}
......@@ -147,10 +147,10 @@ is inspired from~\cite{ayad10ijcar}.
\item[Append] function \verb|append|, concatenation of lists.
\item[Reverse] function \verb|reverse| for list reversal.
\item[Sorted] predicate \verb|sorted| for lists of integers.
\item[NumOcc] number of occurrences in a list
\item[Permut] list permutations
\item[Induction] structural induction on lists
\item[Map] list map operator
\item[NumOcc] number of occurrences in a list.
\item[Permut] list permutations.
\item[Induction] structural induction on lists.
\item[Map] list map operator.
\end{description}
......
......@@ -8,30 +8,31 @@ Compilation of \why\ must start with a configuration phase which is run as
\begin{verbatim}
./configure
\end{verbatim}
This analyzes you current configuration and check if requirements hold.
This analyzes your current configuration and checks if requirements hold.
Compilation requires:
\begin{itemize}
\item The Objective Caml compiler, version 3.10 or higher. It is
available as a binary package for most Unix distributions. For
debian-based Linux distributions, you can install the packages
Debian-based Linux distributions, you can install the packages
\begin{verbatim}
ocaml ocaml-native-compilers
\end{verbatim}
It is also installable from sources, downloadable from the Web site
It is also installable from sources, downloadable from the site
\url{http://caml.inria.fr/ocaml/}
\end{itemize}
For the IDE, additional Ocaml libraries are needed:
For the IDE, additional OCaml libraries are needed:
\begin{itemize}
\item The Lablgtk2 library for Ocaml bindings of the gtk2 graphical library.
For debian-based Linux distributions, you can install the packages
\item The Lablgtk2 library for OCaml bindings of the gtk2 graphical library.
For Debian-based Linux distributions, you can install the packages
\begin{verbatim}
liblablgtk2-ocaml-dev liblablgtksourceview2-ocaml-dev
\end{verbatim}
It is also installable from sources, available from the site \url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}
It is also installable from sources, available from the site
\url{http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html}
\item The Ocaml bindings of the sqlite3 library
For debian-based Linux distributions, you can install the package
\item The OCaml bindings of the sqlite3 library.
For Debian-based Linux distributions, you can install the package
\begin{verbatim}
libsqlite3-ocaml-dev
\end{verbatim}
......@@ -39,9 +40,15 @@ It is also installable from sources, available from the site
\url{http://ocaml.info/home/ocaml_sources.html#ocaml-sqlite3}
\end{itemize}
When configuration is finished, you can compile \why.
\begin{verbatim}
make
\end{verbatim}
\subsection{Local use, without installation}
It is not mandatory to install \why\ to use it. Local use is obtained via
It is not mandatory to install \why\ into system directories.
\why\ can be configured and compiled for local use as follows:
\begin{verbatim}
./configure --enable-local
make
......@@ -67,7 +74,7 @@ installing Why.
For installation of external provers, please look at the Why provers
tips page \url{http://why.lri.fr/provers.en.html}.
For configuring \why\ to use the provers, follow intructions given in
For configuring \why\ to use the provers, follow instructions given in
Section~\ref{sec:why3config}.
\section{The \texttt{why3config} command-line tool}
......@@ -82,9 +89,9 @@ or using the menu
\begin{verbatim}
File/Detect provers
\end{verbatim}
of the IDE. This must be done again each time a new prover is installed.
of the IDE. This must be redone each time a new prover is installed.
The set of all provers which are attempted to detect is described in
The provers which \why\ attempts to detect are described in
the readable configuration file \texttt{provers-detection-data.conf}
of the \why\ data directory (\eg{}
\texttt{/usr/local/share/why3}). Advanced users may try to modify this
......@@ -93,12 +100,12 @@ please consider submitting a new prover configuration on the bug
tracking system).
The result of the prover detection is stored in the user's
configuration file (\eg{} \texttt{~/.why.conf}). Again, this file is
human readable, and advanced users may modify it in order to
experiment different ways of calling provers, \eg{} different versions
of the same prover, or with different options.
configuration file (\eg{} \verb+~/.why.conf+). Again, this file
is human-readable, and advanced users may modify it in order to
experiment with different ways of calling provers, \eg{} different
versions of the same prover, or with different options.
The provers which are typically attemped for detection are
The provers which are typically looked for are
\begin{itemize}
\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/}
......@@ -118,54 +125,60 @@ 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
provers and will replace them in the file configuration.
\texttt{why3config} will only reset unset variables to default value,
but will not try to detect provers.
The option \texttt{--autodetect-provers} should be used to force
\why\ to detect again the available
provers and to replace them in the configuration file. The option
\texttt{--autodetect-plugins} will do the same for plugins.
\section{The \texttt{why3} command-line tool}
\label{sec:why3ref}
\why\ is primarily used to call provers on goals contains by file in
why3 format \texttt{.why} extension. However plugins can register
parser which can extend the known format. \texttt{why3ml} apply the
following steps :
\why\ is primarily used to call provers on goals contained in an
input file. By default, such a file must be written in \why language
and have the extension \texttt{.why}. However, a dynamically loaded
plugin can register a parser for some other format of logical problems,
\eg{} TPTP or SMTlib.
The \texttt{why3} tool executes the following steps:
\begin{enumerate}
\item Parse the command line and report error if needed
\item Parse the command line and report errors if needed.
\item Read the configuration file using the priority defined in
section\ref{sec:whyconffile}
\item Load the plugins mentionned in the configuration. It will not
stop if a plugin fail to load.
\item Parse and type the given files using the correct parser in order
to obtain a set of why theory for each files. It uses
the filename extension or the \texttt{--format} options to choose
among the available parsers. \texttt{--list-format} gives the list
of them.
\item Extract the selected goals inside each selected theories into
tasks. The goals and theories are selected using the options
\texttt{-G/--goal} and \texttt{-T/--theory}. One
Section~\ref{sec:whyconffile}.
\item Load the plugins mentioned in the configuration. It will not
stop if some plugin fails to load.
\item Parse and typecheck the given files using the correct parser in order
to obtain a set of \why\ theories for each file. It uses
the filename extension or the \texttt{--format} option to choose
among the available parsers. The \texttt{--list-format} option gives
the list of registered parsers.
\item Extract the selected goals inside each of the selected theories
into tasks. The goals and theories are selected using the options
\texttt{-G/--goal} and \texttt{-T/--theory}. The option
\texttt{-T/--theory} applies to the last file appearing on the
commandline, one \texttt{-G/--goal} applies to the last theory
appearing on the commandline. If none theories are selected in one
file, they are all selected. If none goals are selected inside one
selected theory, they are all selected.
command line, the option \texttt{-G/--goal} applies to the last theory
appearing on the command line. If no theories are selected in a file,
then every theory is considered as selected. If no goals are selected
in a theory, then every goal is considered as selected.
\item Apply the transformation requested
with \texttt{-a/--apply-transform} in the order they appear on the
with \texttt{-a/--apply-transform} in their order of appearance on the
command line. \texttt{--list-transforms} list the known
transformations, plugins can add more of them.
\item Apply the driver selected with the \texttt{-D/--driver} option,
or the driver of the prover selected with \texttt{-P/--prover}
option. \texttt{--list-provers} lists the known provers, ie the one
option. \texttt{--list-provers} lists the known provers, i.e.~the ones
which appear in the configuration file.
\item Print the result of the standard output if \texttt{-D/--driver}
is used or call the prover and print the result if
\texttt{-P/--prover} is used.
\item If the option \texttt{-P/--prover} is given, call the selected prover
on each generated task and print the results. If the option
\texttt{-D/--driver} is given, print each generated task using
the format specified in the selected driver.
\end{enumerate}
\texttt{why3} call the prover sequentially, use \texttt{why3bench} if *)
you want to call the provers concurrently. *)
%\texttt{why3} calls the provers sequentially, use \texttt{why3bench} if *)
%you want to call the provers concurrently. *)
The provers can answer the following output :
The provers can answer the following output:
\begin{itemize}
\item[Valid] the goal is proved in the given context,
\item[Unknown] the prover stop by itself to search,
......
......@@ -94,13 +94,14 @@ $^2$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
This is the manual for the Why platform version 3, or \why\ for
short. \why\ 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
external prover if wanted. A major new feature is also the ability
to use Why programmatically, via a well-designed API.
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\
formalisations or to add support for a new external
prover if wanted.
\subsection*{Availability}
......@@ -132,17 +133,17 @@ Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.
\section*{Release notes}
\paragraph{Version 0.10}