Commit 9585835c authored by MARCHE Claude's avatar MARCHE Claude

doc: updated examples for why3session command

parent ab97a29f
\begin{tabular}{| l |c |c |c |c |c |}
\hline Proof obligations & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\
\hline
\explanation{G1} & \noresult& \noresult& \valid{0.00} \\
\hline
\explanation{G2} & \unknown{0.00} & \noresult& \unknown{0.00} \\
\cline{2-4}
\quad\transformation{split\_goal} & \multicolumn{3}{|c|}{}\\
\cline{2-4}
\quad\subgoal{1.}{1} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\
\cline{2-4}
\quad\subgoal{2.}{2} & \valid{0.00} & \noresult& \valid{0.00} \\
\hline
\explanation{G3} & \valid{0.00} & \noresult& \unknown{0.00} \\
\begin{tabular}{|l|l|l|l|c|c|}
\hline Proof obligations & \provername{Alt-Ergo 0.99.1} & \provername{Coq 8.7.1} \\
\hline
\explanation{G1} & \valid{0.00} & \noresult\\
\hline
\explanation{G2} & \unknown{0.00} & \noresult\\
\cline{2-3}
\quad\transformation{split\_goal\_right} & \multicolumn{2}{|c|}{}\\
\cline{2-3}
\quad\subgoal{G2.0}{1} & \unknown{0.00} & \unknown{0.29} \\
\cline{2-3}
\quad\subgoal{G2.1}{2} & \valid{0.00} & \noresult\\
\hline
\explanation{G3} & \valid{0.00} & \noresult\\
\hline \end{tabular}
\begin{tabular}{| l |c |c |c |c |c |}
\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo (0.94)} & \provername{Coq (8.3pl4)} & \provername{Simplify (1.5.4)} \\
\hline
\explanation{G1} & & \noresult& \noresult& \valid{0.00} \\
\hline
\explanation{G2} & & \unknown{0.00} & \noresult& \unknown{0.00} \\
\cline{2-4}
& \explanation{1.} & \unknown{0.00} & \unknown{0.43} & \unknown{0.00} \\
\cline{2-5}
& \explanation{2.} & \valid{0.00} & \noresult& \valid{0.00} \\
\hline
\explanation{G3} & & \valid{0.00} & \noresult& \unknown{0.00} \\
\begin{tabular}{|l|l|l|l|c|c|}
\hline \multicolumn{2}{|c|}{Proof obligations } & \provername{Alt-Ergo 0.99.1} & \provername{Coq 8.7.1} \\
\hline
\explanation{G1} & & \valid{0.00} & \noresult\\
\hline
\explanation{G2} & & \unknown{0.00} & \noresult\\
\cline{2-3}
& \explanation{G2.0} & \unknown{0.00} & \unknown{0.29} \\
\cline{2-4}
& \explanation{G2.1} & \valid{0.00} & \noresult\\
\hline
\explanation{G3} & & \valid{0.00} & \noresult\\
\hline \end{tabular}
doc/hello_proof.png

20.7 KB | W: | H:

doc/hello_proof.png

20.3 KB | W: | H:

doc/hello_proof.png
doc/hello_proof.png
doc/hello_proof.png
doc/hello_proof.png
  • 2-up
  • Swipe
  • Onion skin
......@@ -719,8 +719,9 @@ about the session, depending on the following specific options.
the session as edited proofs.
\item[\texttt{-{}-stats}] prints various proofs statistics, as
detailed below.
\item[\texttt{-{}-tree}] prints the structure of the session as a
tree in ASCII, as detailed below.
% OBSOLETE
% \item[\texttt{-{}-tree}] prints the structure of the session as a
% tree in ASCII, as detailed below.
\item[\texttt{-{}-print0}] separates the results of the options
\verb|provers| and \verb|--edited-files| by the character number 0
instead of end of line \verb|\n|. That allows you to safely use
......@@ -739,36 +740,39 @@ why3 session info --edited-files --print0 vstte12_bfs.mlw | \
\end{description}
\paragraph{Session Tree}
The hierarchical structure of the session is printed as a tree in
ASCII. The files, theories, goals are marked with a question mark
\verb|?|, if they are not verified. A proof is usually said to be
verified if the proof result is \verb|valid| and the proof is not
obsolete.
However here specially we separate these two properties. On
the one hand if the proof suffers from an internal failure we mark it
with an exclamation mark \verb|!|, otherwise if it is not valid we
mark it with a question mark \verb|?|, finally if it is valid we add
nothing. On the other hand if the proof is obsolete we mark it with an
\verb|O|.
For example, here are the session tree produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
{\scriptsize
\begin{verbatim}
hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
| `-Alt-Ergo (0.94)
|-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
| | | `-Alt-Ergo (0.94)
| | `-G2.1?-+-Coq (8.3pl4)?
| | |-Simplify (1.5.4)?
| | `-Alt-Ergo (0.94)?
| |-Simplify (1.5.4)?
| `-Alt-Ergo (0.94)?
`-G1---Simplify (1.5.4)
\end{verbatim}
}
% OBSOLETE
% \paragraph{Session Tree}
% The hierarchical structure of the session is printed as a tree in
% ASCII. The files, theories, goals are marked with a question mark
% \verb|?|, if they are not verified. A proof is usually said to be
% verified if the proof result is \verb|valid| and the proof is not
% obsolete.
% However here specially we separate these two properties. On
% the one hand if the proof suffers from an internal failure we mark it
% with an exclamation mark \verb|!|, otherwise if it is not valid we
% mark it with a question mark \verb|?|, finally if it is valid we add
% nothing. On the other hand if the proof is obsolete we mark it with an
% \verb|O|.
% For example, here are the session tree produced on the ``hello
% proof'' example of Section~\ref{chap:starting}.
% {\scriptsize
% \begin{verbatim}
% hello_proof---../hello_proof.why?---HelloProof?-+-G3-+-Simplify (1.5.4)?
% | `-Alt-Ergo (0.94)
% |-G2?-+-split_goal?-+-G2.2-+-Simplify (1.5.4)
% | | | `-Alt-Ergo (0.94)
% | | `-G2.1?-+-Coq (8.3pl4)?
% | | |-Simplify (1.5.4)?
% | | `-Alt-Ergo (0.94)?
% | |-Simplify (1.5.4)?
% | `-Alt-Ergo (0.94)?
% `-G1---Simplify (1.5.4)
% \end{verbatim}
% }
\paragraph{Session Statistics}
......@@ -794,27 +798,31 @@ For example, here are the session statistics produced on the ``hello
proof'' example of Section~\ref{chap:starting}.
{\footnotesize
\begin{verbatim}
== Number of goals ==
total: 5 proved: 3
== Number of root goals ==
total: 3 proved: 2
== Number of sub goals ==
total: 2 proved: 1
== Goals not proved ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G2
+-- transformation split_goal
+-- goal G2.1
+-- transformation split_goal_right
+-- goal G2.0
== Goals proved by only one prover ==
+-- file ../hello_proof.why
+-- theory HelloProof
+-- goal G1: Simplify (1.5.4) (0.00)
+-- goal G3: Alt-Ergo (0.94) (0.00)
+-- goal G1: Alt-Ergo 0.99.1
+-- goal G2
+-- transformation split_goal_right
+-- goal G2.1: Alt-Ergo 0.99.1
+-- goal G3: Alt-Ergo 0.99.1
== Statistics per prover: number of proofs, time (minimum/maximum/average) in seconds ==
Alt-Ergo (0.94) : 2 0.00 0.00 0.00
Simplify (1.5.4) : 2 0.00 0.00 0.00
\end{verbatim}
Alt-Ergo 0.99.1 : 3 0.00 0.00 0.00
\end{verbatim}
}
\subsection{Command \texttt{latex}}
......@@ -910,14 +918,14 @@ override this default).
\begin{htmlonly}
\begin{rawhtml}
<h1>Why3 Proof Results for Project "hello_proof"</h1>
<h2><font color="#FF0000">Theory "HelloProof": not fully verified</font></h2>
<table border="1"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo (0.94)</td><td text-rotation="90">Coq (8.3pl4)</td><td text-rotation="90">Simplify (1.5.4)</td></td></tr>
<td bgcolor="#C0FFC0" colspan="2">G1</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
<td bgcolor="#FF0000" colspan="2">G2</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
<tr><td bgcolor="#FF0000" colspan="2">split_goal</td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td></tr>
<td rowspan="2">&nbsp;&nbsp;</td><td bgcolor="#FF0000" colspan="1">1.</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#FF8000">0.43</td><td bgcolor="#FF8000">0.00</td></tr>
<tr><td bgcolor="#C0FFC0" colspan="1">2.</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
<td bgcolor="#C0FFC0" colspan="2">G3</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
<h2><span style="color:#FF0000">Theory "hello_proof.HelloProof": not fully verified</span></h2>
<table border="1" style="border-collapse:collapse"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo 0.99.1</td><td text-rotation="90">Coq 8.7.1</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">G1</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#FF0000" colspan="2">G2</td><td style="background-color:#FF8000">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#FF0000" colspan="2">split_goal_right</td><td style="background-color:#E0E0E0"></td><td style="background-color:#E0E0E0"></td></tr>
<tr><td rowspan="2" style="width:1ex"></td><td style="background-color:#FF0000" colspan="1">G2.0</td><td style="background-color:#FF8000">0.00</td><td style="background-color:#FF8000">0.29</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="1">G2.1</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
<tr><td style="background-color:#C0FFC0" colspan="2">G3</td><td style="background-color:#C0FFC0">0.00</td><td style="background-color:#E0E0E0">---</td></tr>
</table>
\end{rawhtml}
\end{htmlonly}
......
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