Commit 12b6e17f authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix some documentation typos.

parent db9ccd3d
......@@ -141,8 +141,8 @@ The \texttt{why3} tool executes the following steps:
\whyml modules are turned into
theories containing verification conditions as goals.
\item Extract the selected goals inside each of the selected theories
into tasks. The goals and theories are selected using the options
\verb|-G/--goal| and \verb|-T/--theory|. The option
into tasks. The goals and theories are selected using options
\verb|-G/--goal| and \verb|-T/--theory|. Option
\verb|-T/--theory| applies to the last file appearing on the
command line, the option \verb|-G/--goal| applies to the last theory
appearing on the command line. If no theories are selected in a file,
......@@ -154,21 +154,21 @@ The \texttt{why3} tool executes the following steps:
\index{theory@\verb+--theory+}
\item Apply the transformation requested
with \verb|-a/--apply-transform| in their order of appearance on the
command line. \verb|--list-transforms| list the known
command line. \verb|--list-transforms| lists the known
transformations, plugins can add more of them.
\index{a@\verb+-a+|see{\texttt{-{}-apply-transform}}}
\index{apply-transform@\verb+--apply-transform+}
\index{list-transforms@\verb+--list-transforms+}
\item Apply the driver selected with the \verb|-D/--driver| option,
or the driver of the prover selected with \verb|-P/--prover|
or the driver of the prover selected with the \verb|-P/--prover|
option. \verb|--list-provers| lists the known provers, \ie the ones
that appear in the configuration file.
\index{D@\verb+-D+|see{\texttt{-{}-driver}}}
\index{driver@\verb+--driver+}
\index{P@\verb+-P+|see{\texttt{-{}-prover}}}
\index{prover@\verb+--prover+}
\item If the option \verb|-P/--prover| is given, call the selected prover
on each generated task and print the results. If the option
\item If option \verb|-P/--prover| is given, call the selected prover
on each generated task and print the results. If option
\verb|-D/--driver| is given, print each generated task using
the format specified in the selected driver.
\end{enumerate}
......@@ -179,11 +179,11 @@ The \texttt{why3} tool executes the following steps:
\noindent
The provers can give the following output:
\begin{description}
\item[Valid] the goal is proved in the given context,
\item[Unknown] the prover has stopped its search,
\item[Timeout] the prover has reached the time limit,
\item[Failure] an error has occurred,
\item[Invalid] the prover knows the goal cannot be proved.
\item[Valid] The goal is proved in the given context.
\item[Unknown] The prover has stopped its search.
\item[Timeout] The prover has reached the time limit.
\item[Failure] An error has occurred.
\item[Invalid] The prover knows the goal cannot be proved.
\end{description}
% \why can also be *)
% used to provide other informations : *)
......@@ -193,12 +193,12 @@ The provers can give the following output:
% \item TO BE COMPLETED *)
% \end{itemize} *)
The option \verb|--bisect| changes the behavior of why3. With this
Option \verb|--bisect| changes the behavior of why3. With this
option, \verb|-P/--prover| and \verb|-o/--output| must be given
and a valid goal must be selected. The last step executed by why3 is
replaced by computing a minimal set (in the great majority of the
case) of declarations that still prove the goal. Currently it does not
use any information provided by the prover, it call the prover
use any information provided by the prover; it calls the prover
multiple times with reduced context. The minimal set of declarations is
then written in the prover syntax into a file located in the directory
given to the \verb|-o/--output| option.
......@@ -224,42 +224,42 @@ time limit and memory limit given, and the result of the prover. The
result of the prover is the same as when you run the why3 tool. It
contains the time taken and the state of the proof:
\begin{itemize}
\item \texttt{Valid}: the task is valid according to the prover. The
\begin{description}
\item[Valid] The task is valid according to the prover. The
goal is considered proved.
\item \texttt{Invalid}: the task is invalid.
\item \texttt{Timeout}: the prover exceeded the time limit.
\item \texttt{OufOfMemory}: the prover exceeded the memory limit.
\item \texttt{Unknown}: the prover can't determine if the task
is valid; Some additional information can be provided.
\item \texttt{Failure}: the prover reports a failure.
\item \texttt{HighFailure}: an error occurred while trying to call the
\item[Invalid] The task is invalid.
\item[Timeout] the prover exceeded the time limit.
\item[OufOfMemory] The prover exceeded the memory limit.
\item[Unknown] The prover cannot determine if the task
is valid. Some additional information can be provided.
\item[Failure] The prover reported a failure.
\item[HighFailure] An error occurred while trying to call the
prover, or the prover answer was not understood.
\end{itemize}
\end{description}
Additionally a proof attempt can have the following attribute:
Additionally, a proof attempt can have the following attributes:
\begin{itemize}
\item obsolete:\index{obsolete!proof attempt} the prover associated to
that proof attempt has not been run on the current task, but on a
\begin{description}
\item[obsolete]\index{obsolete!proof attempt} The prover associated to
that proof attempt has not been run on the current task, but on an
earlier version of that task. You need to replay the proof
attempt, \emph{i.e.} run the prover with the current task of the proof
attempt, in order to update the answer of the prover and remove this
attribute.
\item archived:\index{archived!proof attempt} the proof attempt is not useful
anymore it is kept for history, no why3 tools will select it by
default. The section \ref{sec:uninstalledprovers} shows an example
of its usage.
\end{itemize}
\item[archived]\index{archived!proof attempt} The proof attempt is not useful
anymore; it is kept for history; no why3 tools will select it by
default. Section \ref{sec:uninstalledprovers} shows an example
of this usage.
\end{description}
Generally proof attempt are marked obsolete just after
Generally, proof attempts are marked obsolete just after
the start of why3ide. Indeed when you load a session in order to
modify it (not with \texttt{why3session info} for instance), why3
rebuilds the goals to prove by using the information provided in the
session. If you modify the original file (.why, .mlw) or if the
transformations have changed (new version of why3) why3 will detect
that. The provers will perhaps answer differently on this new
problems. So the proof attempts that corresponds to a goal that
transformations have changed (new version of why3), why3 will detect
that. The provers will perhaps answer differently on these new
problems. So the proof attempts that correspond to a goal that
changed are marked obsolete.
% non
......@@ -333,7 +333,7 @@ changed are marked obsolete.
\begin{description}
\item[Expand All] expands all the rows of the tree view.
\item[Collapse proved goals] closes all the rows of the tree view
which are proved.
that are proved.
% \item[Hide proved goals] completely hides the proved rows of the tree
% view [EXPERIMENTAL]
\end{description}
......@@ -343,11 +343,11 @@ A copy of the tools already available in the left toolbar, plus:
\begin{description}
\item[Mark as obsolete] marks all the proof as
obsolete.
This allows to replay every proofs.
\item[Apply non-splitting transformation] apply one of the available
This allows to replay every proof.
\item[Non-splitting transformation] applies one of the available
transformations, as listed in Section~\ref{sec:transformations}
\item[Apply non-splitting transformation]. Same as above, but for
splitting transformations, \emph{i.e.} those that can generated
\item[Splitting transformation] is the same as above, but for
splitting transformations, \emph{i.e.} those that can generate
several sub-goals.
\end{description}
......@@ -357,8 +357,8 @@ A very short online help, and some information about this software.
\subsection{Preferences Dialog}
The preferences dialog allows you to customize various settings. These
are groups together under several tabs
The preferences dialog allows you to customize various settings. They
are grouped together under several tabs.
\begin{description}
\item[\textsf{General Settings} tab] allows one to set
......@@ -432,20 +432,20 @@ of a theory. For that goal it tries to prove predefined goals using
each component to compare. \texttt{why3bench} allows to output the
comparison in various formats:
\begin{itemize}
\item csv: the simpler and more informative format, the results are
represented in an array, the rows corresponds to the
\item csv: the simpler and more informative format; the results are
represented in an array; the rows correspond to the
compared components, the columns correspond to the result
(Valid, Unknown, Timeout, Failure, Invalid) and the CPU time taken in seconds.
\item average: summarizes the number of the five different answers
for each component. It also gives the average time taken.
\item timeline: for each component it gives the number of valid goals
\item timeline: for each component, it gives the number of valid goals
along the time (10 slices between 0 and the longest time a component
takes to prove a goal)
\end{itemize}
The compared components can be defined in an \emph{rc-file},
The compared components can be defined in an \emph{rc-file};
\texttt{examples/programs/\ prgbench.rc} is such an example. More
generally a bench configuration file:
generally, a bench configuration file looks like
\begin{verbatim}
[probs "myprobs"]
file = "examples/mygoal.why" #relatives to the rc file
......
......@@ -753,7 +753,7 @@ to show that the invariant over lengths is maintained, and finally
observes an abstract queue given by a sequence.
\end{quote}
In a new module, we import arithmetic and theory
\texttt{list.ListRich}, a combo theory which imports all list
\texttt{list.ListRich}, a combo theory that imports all list
operations we will require: length, reversal, and concatenation.
\begin{whycode}
module AmortizedQueue
......@@ -776,7 +776,7 @@ or modified in a program.
For the purpose of the specification, it is convenient to introduce a function
\texttt{sequence} which builds the sequence of elements of a queue, that
is the front list concatenated to reversed rear list.
is the front list concatenated to the reversed rear list.
\begin{whycode}
function sequence (q: queue 'a) : list 'a = q.front ++ reverse q.rear
\end{whycode}
......
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