Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
Why3
why3
Commits
bf1abbb6
Commit
bf1abbb6
authored
Mar 30, 2017
by
MARCHE Claude
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
doc proof reading
parent
f6862c01
Changes
4
Hide whitespace changes
Inline
Sidebyside
Showing
4 changed files
with
112 additions
and
77 deletions
+112
77
doc/manpages.tex
doc/manpages.tex
+37
37
doc/manual.bib
doc/manual.bib
+33
18
doc/qualid.bnf
doc/qualid.bnf
+16
12
doc/syntaxref.tex
doc/syntaxref.tex
+26
10
No files found.
doc/manpages.tex
View file @
bf1abbb6
...
...
@@ 216,7 +216,7 @@ The provers can give the following output:
\label
{
sec:proveoptions
}
\begin{description}
\item
[\texttt{{}getce}]
activates the generation of a potential
\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
...
...
@@ 473,25 +473,25 @@ are grouped together under several tabs.
\subsection
{
Displaying Counterexamples
}
When the selected prover finds (counterexample) model, it is possible to
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
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
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
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
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
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}
...
...
@@ 504,7 +504,7 @@ theory T
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" .
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 *)
...
...
@@ 516,9 +516,9 @@ theory T
(* (= (+ (+ 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
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:
...
...
@@ 535,9 +535,9 @@ The following example shows a counterexample of a function with postcondition:
(* 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
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}
...
...
@@ 547,31 +547,31 @@ instead of default prefix notation:
(* 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
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
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
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
...
...
@@ 579,16 +579,16 @@ counterexample of an abstract value:
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
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
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
{
sefm
16
}
.
More information how counterexamples in Why3 works can be found
in~
\cite
{
hauzar16
sefm
}
.
%
% how to use counterexamples  explain labels, projections, the option getce of why3prove and the setting in why3ide
...
...
doc/manual.bib
View file @
bf1abbb6
...
...
@@ 198,7 +198,7 @@ Claude March\'e and Andrei Paskevich},
month
=
{August}
,
url
=
{http://proval.lri.fr/submissions/boogie11.pdf}
,
abstract
=
{Why3 is the next generation of the
Why software verification platform.
Why software verification platform.
Why3 clearly separates the purely logical
specification part from generation of verification conditions for programs.
This article focuses on the former part.
...
...
@@ 232,21 +232,36 @@ 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}
,
@InProceedings
{
hauzar16sefm
,
topics
=
{team}
,
xeditorialboard
=
{yes}
,
xinternationalaudience
=
{yes}
,
xproceedings
=
{yes}
,
xpdf
=
{http://www.lri.fr/~melquion/doc/08rnc8article.pdf}
}
\ No newline at end of file
author
=
{Hauzar, David and March\'e, Claude and Moy, Yannick}
,
title
=
{Counterexamples from Proof Failures in {SPARK}}
,
booktitle
=
{Software Engineering and Formal Methods}
,
year
=
2016
,
pages
=
{215233}
,
hal
=
{https://hal.inria.fr/hal01314885}
}
@techreport
{
ieee7542008
,
abstract
=
{This standard specifies interchange and arithmetic
formats and methods for binary and decimal
floatingpoint arithmetic in computer programming
environments. This standard specifies exception
conditions and their default handling. An
implementation of a floatingpoint system conforming
to this standard may be realized entirely in
software, entirely in hardware, or in any
combination of software and hardware. For operations
specified in the normative part of this standard,
numerical results and exceptions are uniquely
determined by the values of the input data, sequence
of operations, and destination formats, all under
user control.}
,
booktitle
=
{{IEEE} Std 7542008}
,
doi
=
{10.1109/IEEESTD.2008.4610935}
,
journal
=
{IEEE Std 7542008}
,
pages
=
{158}
,
title
=
{{IEEE} Standard for FloatingPoint Arithmetic}
,
year
=
{2008}
}
doc/qualid.bnf
View file @
bf1abbb6
...
...
@@ 3,27 +3,31 @@
\
ualpha ::= "A""Z"
\
digitorus ::= "0""9"  "_"
alpha ::= lalpha  ualpha
\
alphanous ::= "a""z"  "A""Z"
suffix ::= (alpha  digit  "'")*
\
suffix
::=
(
alpha
nous  "'"* digitorus)* "\"*
lident
::=
l
alpha
suffix
\
l
ident
nq
::=
l
alpha suffix
u
ident ::=
u
alpha suffix
\
u
ident
nq
::=
ualpha suffix
ident ::=
lident  uident
\
l
ident
::= lident
("'" alphanous suffix)+
l
qualid
::= lident
 uqualid "." lident
\
u
ident
::= uident
("'" alphanous suffix)+
u
qualid
::= uident
 uqualid "." uident
\
identnq
::=
l
ident
nq
 uident
nq
qualid
::= ident  u
qualid "."
ident
\
ident ::= lident  uident
digitorus ::= "0""9"  "_"
\
lqualid ::= lident  uqualid "." lident
alphanous ::= "a""z"  "A""Z"
\
uqualid ::= uident  uqualid "." uident
suffixnq ::= (alphanous  "'"* digitorus)* "'"*
\
lidentnq ::= lalpha suffixnq
\
uidentnq ::= ualpha suffixnq
\
qualid
::= ident  u
qualid "."
ident ;%
identnq
::=
l
ident
nq
 uident
nq
;%
\end{syntax}
doc/syntaxref.tex
View file @
bf1abbb6
...
...
@@ 24,12 +24,23 @@ In the following, strings are referred to with the nonterminal
\subsection
{
Identifiers
}
The syntax distinguishes lowercase and
uppercase identifi
er
s
and
, similarly, lowercase and uppercase
qualified identifiers
.
Identifiers are nonempty sequences of characters among letters,
digits, the underscore charact
er and
the quote character. They cannot
start with a digit or a quote
.
\begin{center}
\framebox
{
\input
{
./qualid
_
bnf.tex
}}
\end{center}
The syntax distinguishes identifiers that start with a lowercase or an
uppercase letter (resp.
\nonterm
{
lident
}{}
and
\nonterm
{
uident
}{}
), and
similarly, lowercase and uppercase qualified identifiers.
The restricted classes of identifiers denoted by
\nonterm
{
lidentnq
}{}
and
\nonterm
{
uidentnq
}{}
correspond to identifiers where the quote
character cannot be followed by a letter. Identifiers where a quote is
followed by a letter are reserved and cannot be used as identifier for
declarations introduced by the user (see Section~
\ref
{
sec:rangetypes
}
).
\subsection
{
Constants
}
The syntax for constants is given in Figure~
\ref
{
fig:bnf:constant
}
.
Integer and real constants have arbitrary precision.
...
...
@@ 124,6 +135,7 @@ TO BE COMPLETED
TO BE COMPLETED
\subsubsection
{
Range types
}
\label
{
sec:rangetypes
}
A declaration of the form
\texttt
{
type r = < range
\textit
{
a b
}
>
}
defines a type that projects into the integer range
...
...
@@ 160,12 +172,12 @@ This type is used in the standard library in the theories
\texttt
{
bv.BV8
}
,
\texttt
{
bv.BV16
}
,
\texttt
{
bv.BV32
}
,
\texttt
{
bv.BV64
}
.
\subsubsection
{
f
loating
point
t
ypes
}
\subsubsection
{
F
loating

point
T
ypes
}
A declaration of the form
\texttt
{
type f = < float
\textit
{
eb sb
}
>
}
defines
the
type of floating
point numbers as specified by the
IEEE754 standard
. Here the literal
\texttt
{
\textit
{
eb
}}
represents
the number of bits in the exponent and the literal
defines
a
type of floating

point numbers as specified by the
IEEE754
standard~
\cite
{
ieee754
}
. Here the literal
\texttt
{
\textit
{
eb
}}
represents
the number of bits in the exponent and the literal
\texttt
{
\textit
{
sb
}}
the number of bits in the significand (including
the hidden bit). Note that in order to make such a declaration the
theory
\texttt
{
real.Real
}
must be imported.
...
...
@@ 183,9 +195,13 @@ Defining such a type \texttt{f} automatically introduces the following:
constant f'eb : int
constant f'sb : int
\end{whycode}
The predicate
\texttt
{
f'isFinite
}
is the finitness predicate associated to
the float format. The function
\texttt
{
f'real
}
projects a finite term of type
\texttt
{
f
}
to its real value, it is not specified for non finite terms.
As specified by the IEEE standard, float formats includes infinite
values and also a special NaN value (NotaNumber) to represent
results of undefined operations such as
$
0
/
0
$
. The predicate
\texttt
{
f'isFinite
}
indicates whether its argument is neither infinite
nor NaN. The function
\texttt
{
f'real
}
projects a finite term of type
\texttt
{
f
}
to its real value, its result is not specified for non finite
terms.
Unless specified otherwise with the meta
\texttt
{
"keep:literal"
}
on
\texttt
{
f
}
, the transformation
\emph
{
eliminate
\_
literal
}
will
...
...
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