From db678d4e96a1a97431e78cb5865cb8310019d288 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 17 May 2019 11:10:22 +0200
Subject: [PATCH] [wp] improved manual for using Why-3
---
src/plugins/wp/doc/manual/wp_plugin.tex | 90 ++++++++++++++++---------
1 file changed, 59 insertions(+), 31 deletions(-)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index f1970bf9887..b20427d8549 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -988,7 +988,7 @@ controlled by the following options:
(default is: \texttt{1000}).
\end{description}
-\subsection{Decision Procedures Interface}
+\subsection{Prover Selection}
\label{wp-provers}
The generated proof obligations are submitted to external decision
@@ -1103,41 +1103,69 @@ then save the proof scripts in order to replay them in batch mode.
\item[\tt -wp-coq-project='<name>'] override the \verb+_CoqProject+ file name
for Emacs and Proof General.
\end{description}
-
\hrule
-\paragraph{Why3.}
-Since \textsf{WP} version \verb+0.7+ (Fluorine), native support for \textsf{Why3}
-and \textsf{Why3-Ide} are provided. The older system \textsf{Why}
-\verb+2.x+ is \emph{no} longer supported.
+
+\pagebreak
+\paragraph{Why-3.}
+Native support for \textsf{Why-3} is provided (for versions 1.0 and newer).
+\\
+Support for \textsf{Why-3 IDE} is no longer provided.
\begin{description}
-\item[\tt -wp-prover "why3ide"] runs \textsf{Why3-Ide} with all
- generated goals. On exit, the \textsf{WP} plug-in reads back your
- \textsf{Why3} session and updates the proof obligation status accordingly.
-\item[\tt -wp-prover "<p>"] runs a \textsf{Why3} prover named \texttt{<p>}.
-\item[\tt -wp-prover "why3:<p>"] useful alias when \texttt{"<p>"} can
- be ambiguous. It is actually different to run \texttt{alt-ergo} or \texttt{coq}
- directly from \textsf{WP} or through \textsf{Why3}.
-\item[\tt -wp-detect] lists the provers available with \textsf{Why3}.
- This command calls \texttt{why3 --list-provers} but you have to
- configure \textsf{Why3} on your own before, for instance by using
- \texttt{why3config}. Consult the \textsf{Why3} user manual for details.
- The listed prover names can be directly used with the \texttt{-wp-prover} option.
-\item[\tt -wp-why3='<cmd>'] override the \verb+why3+ command.
+\item[\tt -wp-prover "why3:<p>"] runs a \textsf{Why-3} prover named \texttt{<p>}, and
+ exactly behaves like invoking \verb+why3 prover -P <p>+. The list of prover
+ names \verb+<p>+ must be extracted from the \verb+[alias]+ section of your \textsf{Why-3}
+ configuration, which \verb+frama-c -wp-detect+ does for you (see below).
+\item[\tt -wp-prover "<p>"] can also be used instead of \verb+-wp-prover "why3:<p>"+
+ when \verb+<p>+ is not natively supported by \textsf{WP}, like \texttt{alt-ergo},
+ \texttt{altgr-ergo}, \texttt{coq}, \texttt{coqide}, \texttt{script} and \texttt{tip}.
+\item[\tt -wp-detect] lists the provers available for \textsf{Why-3}.
+ This command can only work if \textsf{why3} API was installed before building and
+ installing \textsf{Frama-C}.
+ The option reads your \textsf{Why-3} configuration and prints the available
+ provers with their \verb+-wp-prover <p>+ code names.
+\item[\tt -wp-why3='<cmd>'] overrides the path to the \verb+why3+ command.
\end{description}
-\paragraph{Sessions.}
-Your \textsf{Why3} session is saved in the \texttt{"project.session"}
-sub-directory of \texttt{-wp-out}. You may run
-\texttt{why3ide} by hand by issuing the following command:
-\begin{shell}
-# why3ide -I <frama-c-share>/wp <out>/project.session
-\end{shell}
+\paragraph{Example of using Why-3.}
+Suppose you have the following configuration:
+
+\begin{logs}
+# frama-c -wp-detect
+[wp] Why3 provers detected:
+ - Alt-Ergo 2.0.0 [why3:alt-ergo,altergo]
+ - CVC4 1.6 [cvc4]
+ - CVC4 1.6 (counterexamples) [cvc4-ce]
+ - Coq 8.9.0 [why3:coq]
+ - Z3 4.6.0 [z3]
+ - Z3 4.6.0 (counterexamples) [z3-ce]
+ - Z3 4.6.0 (noBV) [z3-nobv]
+\end{logs}
-Proof recovering features of \textsf{Why3} are fully available, and
-you can interleave proving from \textsf{WP} with manual runs of
-\texttt{why3ide}. Interactive proofs with \textsf{Why3} are completely
-separated from those managed by the native \textsf{WP} interface with
-\textsf{Coq}.
+Then, to use (for instance) \textsf{CVC4 1.6},
+you can use \verb+-wp-prover cvc4+ (since this name is not conflicting
+with any native prover). Alternatively, you can also use the less ambiguous
+name \verb+-wp-prover why3:cvc4+ if you prefer.
+Similarly, if you want to use \textsf{Z3 4.6.0} without bitvectors, you can use \verb+-wp-prover z3-nobv+
+or \verb+-wp-prover why3:z3-nobv+.
+
+However, to use \textsf{Alt-Ergo 2.0.0} \emph{via} \textsf{Why-3}, you shall use
+\verb+-wp-prover why3:alt-ergo+, since \verb+-wp-prover alt-ergo+ would select
+the native support of \textsf{Alt-Ergo} prover. Finally, since \textsf{Why-3} also provides the alias
+\verb+altergo+ for this prover, \verb+-wp-prover altergo+ will also run it \emph{via} \textsf{Why-3}.
+
+%% \paragraph{Sessions.}
+%% Your \textsf{Why3} session is saved in the \texttt{"project.session"}
+%% sub-directory of \texttt{-wp-out}. You may run
+%% \texttt{why3ide} by hand by issuing the following command:
+%% \begin{shell}
+%% # why3ide -I <frama-c-share>/wp <out>/project.session
+%% \end{shell}
+
+%% Proof recovering features of \textsf{Why3} are fully available, and
+%% you can interleave proving from \textsf{WP} with manual runs of
+%% \texttt{why3ide}. Interactive proofs with \textsf{Why3} are completely
+%% separated from those managed by the native \textsf{WP} interface with
+%% \textsf{Coq}.
\subsection{Generated Proof Obligations}
Your proof obligations are generated and saved to several text
--
GitLab