Commit 5bdfc72c authored by MARCHE Claude's avatar MARCHE Claude

doc: additional explanation for command line in IDE

parent 35c1b010
......@@ -131,6 +131,8 @@ why3.conf
/doc/stdlibdoc/
/doc/texput.log
/doc/extract_ocaml_code
/doc/*__*.ml
/doc/*_bnf.tex
# /lib
/lib/why3-cpulimit
......
Why3 source code elements that should be a part of counterexample must be
explicitly marked with \texttt{"model"} label. The following example shows a
Why3 theory with some terms annotated with the \texttt{model} label and the
generated counterexample in comments:
\begin{whycode}
theory T
use import int.Int
goal g_no_lab_ex : forall x:int. x >= 42 -> x + 3 <= 50
goal g_lab_ex : forall x "model":int. ("model" x >= 42) ->
("model" "model_trace:x+3<=50" x + 3 <= 50)
goal computation_ex : forall x1 "model" x2 "model" x3 "model" .
(* x1 = 1; x2 = 1; x3 = 1 *)
("model" "model_trace: x1 + 1 = 2" x1 + 1 = 2) ->
(* x1 + 1 = 2 = true *)
("model" x2 + 1 = 2) ->
(* (= (+ x2 1) 2) = true *)
("model" x3 + 1 = 2) ->
(* (= (+ x3 1) 2) = true *)
("model" x1 + x2 + x3 = 5)
(* (= (+ (+ x1 x2) x3) 5) = false *)
\end{whycode}
To display counterexample values in assertions the term being asserted must be
labeled with the label \texttt{"model\_vc"}. To display counterexample values
in postconditions, the term in the postcondition must be labeled with the
label \texttt{"model\_vc\_post"}.
The following example shows a counterexample of a function with postcondition:
\begin{whycode}
let incr_ex ( x "model" : ref int ) (y "model" : ref int): unit
(* x = -2; y = -2 *)
ensures { !x = old !x + 2 + !y }
=
y := !y + 1;
(* y = -1 *)
x := !x + 1;
(* x = -1 *)
x := !x + 1
(* x = 0 *)
\end{whycode}
It is also possible to rename counterexample elements using the lable
\texttt{"model\_trace:"}. The following example shows the use of renaming a
counterexample element in order to print the counterexample in infix notation
instead of default prefix notation:
\begin{whycode}
goal g_lab_ex : forall x "model":int. ("model" x >= 42) ->
(* x = 48; (<= 42 x) = true *)
("model" "model_trace:x+3<=50" x + 3 <= 50)
(* x+3<=50 = false *)
\end{whycode}
Renaming counterexample elements is in particular useful when Why3 is used as
intermediate language and to show names of counterexample elements in the
source language instead of showing names of Why3 elements.
Note that if the counterexample element is of a record type, it is also
possible to rename names of the record fields by putting the label
\texttt{model\_trace:} to definitions of record fields. For example:
\begin{whycode}
type r = {f "model_trace:.F" :int; g "model_trace:G" :bool}
\end{whycode}
When a prover is queried for a counterexample value of a term of an abstract
type=, an internal representation of the value is get. To get the concrete
representation, the term must be marked with the label
\texttt{"model\_projected"} and a projection function from the abstract type
to a concrete type must be defined, marked as a projection using the meta
\texttt{"model\_projection"}, and inlining of this function must be disabled
using the meta \texttt{"inline : no"}. The following example shows a
counterexample of an abstract value:
\begin{whycode}
theory A
use import int.Int
type byte
function to_rep byte : int
predicate in_range (x : int) = -128 <= x <= 127
axiom range_axiom : forall x:byte.
in_range (to_rep x)
meta "model_projection" function to_rep
meta "inline : no" function to_rep
goal abstr : forall x "model_projected" :byte. to_rep x >= 42 -> to_rep x
+ 3 <= 50
(* x = 48 *)
\end{whycode}
More examples of using counterexample feature of Why3 can be found in the file
examples/tests/cvc4-models.mlw and examples/tests/cvc4-models.mlw.
More information how counterexamples in Why3 works can be found
in~\cite{hauzar16sefm}.
......@@ -434,6 +434,17 @@ some information about this software.
\end{description}
\subsection{Command-line interface}
Between the top-right zone containing source files and task, and the
bottom-right zone containing various messages, a text input field
allows the user to invoke commands using a textual interface (see
Figure~\ref{fig:gui1}). The 'help' command displays a basic list of
available commands. All commands available in the menus are also
available as a textual command. However the textual interface allows
for much more possibilities, including the ability to invoke
transformations with arguments.
\subsection{Preferences Dialog}
......
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