Commit 56f88378 authored by MARCHE Claude's avatar MARCHE Claude

doc for why3replayer

parent 61f0302d
......@@ -55,31 +55,38 @@
* rename andb, orb, xorb and notb into and, or, xor and not
=== Roadmap for third release 0.70 =======================================
=== Roadmap for third release 0.70, july 2011 ========================
* Final preparation: put on the web page
** why3-0.70.tar.gz
** manual in PDF
** API doc in HTML (suggestion: http://why3.lri.fr/api/)
Note: check that URL of API doc is correct in doc/api.tex line 9.
** What to put in the annoucement
- WhyML VC generator to prove programs
- new tool why3replayer
- incompatible changes in syntax: function, predicate, and, or
- session database in XML format instead of sqlite3
- threads problem in IDE solved (by not using threads anymore)
** as soon as possible: update why3 output of Why2, release Why 2.30
* doc: citer l'article Boogie 2011 quelque part
* increment the magic number in config (A)
* Distribution of examples: we should distribute those who have an xml file
under git, and distribute the XML and Coq proofs
(JC)
* update doc
- why3replay (C) parler des examples distribues ci dessus
* distribute bench files (A + F)
* document new IDE features (C)
* document "Make obsolete" (A)
* Distribution of examples: we should distribute those who have an xml file
under git, and distribute the XML and Coq proofs
(JC)
* (done) update doc for why3replayer
- not done: parler des examples distribues ci dessus
* DONE deplacer le bouton "Cancel" dans le menu "tools",
le renommer en "make obsolete"
......
......@@ -388,6 +388,57 @@ One can run all the bench given in one bench configuration file with
why3bench -B path_to_my_bench.rc
\end{verbatim}
\section{The \texttt{why3replayer} tool}
The purpose of the \texttt{why3replayer} tool is to execute the proofs
stored in a \why session file, as the one produced by the IDE. Its
main goal is to play non-regression tests.
The tool is inkoved in a terminal or a script using
\begin{flushleft}\ttfamily
why3replayer \textsl{[options] <project directory>}
\end{flushleft}
The session file \texttt{why3session.xml} stored in the given
directory is loaded and all the proofs it contains are rerun. Then,
any difference between the information stored in the session file and
the new run are shown.
Nothing is shown when there is no change in the results, independently
of the fact the considered goal is proved or not. When all the proof
runs are done, a summary of what is proved or not is displayed using a
tree-shape pretty print, similar to the IDE tree view after doing
``Collapse proved goals'', that is when a goal, a theory or a file is
fully proved the subtree is not shown.
For example, running the replayer on the \texttt{hello\_proof} example
of Section~\ref{chap:starting} is as follows.
\begin{verbatim}
$ why3replayer hello_proof
Info: found directory 'hello_proof' for the project
Opening session...[Xml warning] prolog ignored
[Reload] file '../hello_proof.why'
[Reload] theory 'HelloProof'
[Reload] transformation split_goal for goal G2
done
Progress: 9/9
2/3
+--file ../hello_proof.why: 2/3
+--theory HelloProof: 2/3
+--goal G2 not proved
Everything OK.
\end{verbatim}
The last line tells us that no difference was detected between the
current run and the informations in the XML file. The tree above
reminds us that the G2 is not proved.
\paragraph{Exit code and options}
\begin{itemize}
\item The exit code is 0 if no difference was detected, 1 if there
was. Other exit codes mean some failure in running the replay.
\item option \texttt{-s}: suppresses the output of the final tree view
\item option \texttt{-I \textsl{<path>}}: suppresses the output of the final tree view
\end{itemize}
\section{The \texttt{why3.conf} configuration file}
\label{sec:whyconffile}
One can use a custom configuration file. \texttt{why3config}
......
......@@ -3,42 +3,42 @@
<why3session name="examples/hello_proof/why3session.xml">
<file name="../hello_proof.why" verified="false" expanded="true">
<theory name="HelloProof" verified="false" expanded="true">
<goal name="G1" sum="f81584706e28397114f2508adf6dd2ff" proved="true" expanded="true">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<goal name="G1" sum="da0794d2f4de035d230d26e93d3e1afe" proved="false" expanded="true">
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="G2" sum="0bb17dc8e6f26a1a6aaf5ecf8ed5a5a8" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<goal name="G2" sum="07e54d9a25fa3174d5d5bf7ce71a13dc" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.01"/>
</proof>
<transf name="split_goal" proved="false" expanded="true">
<goal name="G2.1" sum="54b5fc27ec93fbe413651f6064794e54" proved="false" expanded="true">
<proof prover="coq" timelimit="10" edited="" obsolete="false">
<goal name="G2.1" sum="f7915ef009bdd949e4af326643583051" proved="false" expanded="true">
<proof prover="coq" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.46"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.02"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.01"/>
</proof>
</goal>
<goal name="G2.2" sum="6cdd03a110385f45423b1683748dce81" proved="true" expanded="true">
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<goal name="G2.2" sum="c53f58872dc3cb71805234ace78f1c2d" proved="false" expanded="true">
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
</goal>
<goal name="G3" sum="b3b51b7bb0acfa332bfb937bfa017230" proved="true" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<goal name="G3" sum="8813554ea4313f64f3efc3330036b5e9" proved="false" expanded="true">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="true">
<result status="valid" time="0.01"/>
</proof>
<proof prover="simplify" timelimit="10" edited="" obsolete="false">
<proof prover="simplify" timelimit="10" edited="" obsolete="true">
<result status="unknown" time="0.01"/>
</proof>
</goal>
......
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