Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
54579859
Commit
54579859
authored
Aug 18, 2016
by
David Hauzar
Browse files
Initial documentation of counterexamples.
parent
92ba52cb
Changes
2
Hide whitespace changes
Inline
Sidebyside
doc/manpages.tex
View file @
54579859
...
...
@@ 216,7 +216,8 @@ The provers can give the following output:
\label
{
sec:proveoptions
}
\begin{description}
\item
[\texttt{{}getce}]
activates the generation of a potential counterexample when a proof does not succeed (experimental).
\item
[\texttt{{}getce}]
activates the generation of a potential
counterexample when a proof does not succeed (experimental).
\item
[\texttt{{}extraexplprefix \textsl{<s>}}]
specifies
\textsl
{
s
}
as an additional prefix for labels that denotes VC
explanations. The option can be used several times to specify
...
...
@@ 450,7 +451,125 @@ are grouped together under several tabs.
decision by clicking on it.
\end{description}
% \subsection{Displaying Counterexamples}
\subsection
{
Displaying Counterexamples
}
When the selected prover finds (counterexample) model, it is possible to
display parts of this model in the terms of the original Why3 input.
Currently, this is supported for CVC4 prover version 1.5 and newer.
To display the counterexample in Why3 IDE, the counterexample model generation
must be enabled in File /> Preferences /> get
counterexample.
After running the prover and clicking on the prover result in, the
counterexample can be displayed in the tab
Counterexample.
The counterexample is displayed with the original Why3 code in comments.
Counterexample values for Why3 source code elements at given line are
displayed in a comment at the line below.
An alternative way how to display a counterexample is to use the option
\texttt
{

{}
getce
}
of the
\texttt
{
prove
}
command.
Why3 source code elemets 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/cvc4models.mlw and examples/tests/cvc4models.mlw.
More information how counterexamples in Why3 works can be found
in~
\cite
{
sefm16
}
.
%
% how to use counterexamples  explain labels, projections, the option getce of why3prove and the setting in why3ide
%
...
...
doc/manual.bib
View file @
54579859
...
...
@@ 232,3 +232,21 @@ Claude March\'e and Andrei Paskevich},
year
=
{2007}
}
@inproceedings
{
sefm16
,
author
=
{Guillaume Melquiond}
,
title
=
{Floatingpoint arithmetic in the {C}oq system}
,
booktitle
=
{Proceedings of the 8th Conference on Real Numbers and
Computers}
,
address
=
{Santiago de Compostela, Spain}
,
year
=
{2008}
,
pages
=
{93102}
,
xequipes
=
{demons PROVAL}
,
xtype
=
{article}
,
xsupport
=
{actes}
,
xclesupport
=
{RNC}
,
topics
=
{team}
,
xeditorialboard
=
{yes}
,
xinternationalaudience
=
{yes}
,
xproceedings
=
{yes}
,
xpdf
=
{http://www.lri.fr/~melquion/doc/08rnc8article.pdf}
}
\ No newline at end of file
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment