Commit 5542328b authored by MARCHE Claude's avatar MARCHE Claude
Browse files

relecture de Claude

parent 3b4d52ab
......@@ -283,27 +283,28 @@ the GUI.
[TO BE COMPLETED LATER]
\section{The \texttt{why3bench} tool}
The \texttt{why3bench} tool add a scheduler on top of the \why\
The \texttt{why3bench} tool adds a scheduler on top of the \why\
library. \texttt{why3bench} is designed to compare various composants
of automatic proofs : automatic provers, transformations, definitions
of one theory. For that goal it tries to prove predefined goals using
each composants to compare. \texttt{why3bench} allows to output the
comparison in various formats :
of automatic proofs: automatic provers, transformations, definitions
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
\item csv: the simpler and more informative format, the results are
represented in an array, the rows corresponds to the
compared composants, the columns corresponds to the result
(Valid,Unknown,Timout,Failure,Invalid) and the cpu time taken in seconds.
\item average : summarize the number of the five differents answers
for each composants. It also gives the average time taken.
\item timeline : for each composants it gives the number of goal valid
along the time (10 slices between 0 and the longest time a composant
take to prove a goal)
compared components, the columns correspond to the result
(Valid,Unknown,Timout,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
along the time (10 slices between 0 and the longest time a component
takes to prove a goal)
\end{itemize}
The compared composants 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:
\begin{verbatim}
[probs "myprobs"]
file = "examples/monbut.why" #relatives to the rc file
......@@ -342,14 +343,14 @@ generally a bench configuration file :
csv = "prgbench.csv"
\end{verbatim}
Such file can defined three famillies \texttt{tools,probs,bench}. the
sections \texttt{tools} define a set of composants to compare, the
sections \texttt{probs} define a set of goal on which compare some
composants and the sections \texttt{bench} define which composants to
compare using which goals. It refer by name to the sections
Such a file can defined three families \texttt{tools,probs,bench}. The
sections \texttt{tools} define a set of components to compare, the
sections \texttt{probs} define a set of goals on which to compare some
components and the sections \texttt{bench} define which components to
compare using which goals. It refers by name to the sections
\texttt{tools} and \texttt{probs} defined in the same file. The order
of the definitions is irrelevant. Notice that \texttt{loadpath} in a family
\texttt{tools} can be used to compare differents axiomatisation.
\texttt{tools} can be used to compare different axiomatisation.
One can run all the bench given in one bench configuration file with
\texttt{why3bench} :
......
......@@ -113,7 +113,7 @@ of \texttt{length}): it is unused and therefore optional.
In the previous section we have seen how a theory can reuse the
declarations of another theory, coming either from the same input
text or from the library. Another way to referring to a theory is
by <<cloning>>. A \texttt{clone} declaration constructs a local
by ``cloning''. A \texttt{clone} declaration constructs a local
copy of the cloned theory, possibly instantiating some of its
abstract (i.e.~declared but not defined) symbols.
......
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