Commit 02acc89f authored by MARCHE Claude's avatar MARCHE Claude

fill the file CHANGES plus minor changes in the manual

parent 785df505
* marks an incompatible change
Provers
Language
o two new forms of type declarations: integer range types and
floating-point types. To denote constants in such types, integer
constants and real constants can be cast to such types. This
support is exploited in drivers for provers that support bitvector
theories (CVC4, Z3) and floating-point theory (Z3).
More details in the manual, section 7.2.4 "Theories"
* a quote character (') inside an identifier must either be at the
end, or be followed by either a digit, the underscore character
(_) or another quote. Identifiers with a quote followed by a
letter are reserved.
Standard library
o new theory ieee_float formalizing floating-point arithmetic,
conformant to IEEE-754, mapped to SMT-LIB FP theory.
User features
o proof strategies: why3 config now generates default proof strategies
using the installed provers. These are available under name "Auto
level 0", "Auto level 1" and "Auto level 2" in why3 ide. More
details in the manual, section 10.6 "Proof Strategies"
o counterexamples: better support for array
values, support for floating-point values, support for Z3 in
addition to CVC4.
More details in the manual, section 6.3.5 "Displaying Counterexamples"
Prover support
o support for Isabelle 2017
* discarded support for Isabelle 2016 (2016-1 still supported)
o support for Coq 8.6.1 (released Jul 25, 2017)
o support for CVC4 1.5 (released Jul 10, 2017)
o support for E 2.0 (released Jul 4, 2017)
o support for E 1.9.1 (release Aug 31, 2016)
Tools
o why3 config now generates default proof strategies using the
installed provers. These are available under name "Auto level 1"
and "Auto level 2" in why3 ide.
Version 0.87.3, January 12, 2017
================================
......
......@@ -475,7 +475,7 @@ are grouped together under several tabs.
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.
Currently, this is supported for CVC4 prover version 1.5 and Z3.
To display the counterexample in Why3 IDE, the counterexample model generation
must be enabled in File -/> Preferences -/> get
......@@ -489,7 +489,7 @@ displayed in a comment at the line below.
An alternative way how to display a counterexample is to use the option
\texttt{-{}-get-ce} of the \texttt{prove} command.
Why3 source code elemets that should be a part of counterexample must be
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:
......
......@@ -642,7 +642,7 @@ language are:
To examplify this basic programming language, we give below the
default strategies that are attached to the default buttons of the
IDE, assuming that the provers Alt-Ergo 1.01, CVC4 1.4 and Z3 4.4.1
IDE, assuming that the provers Alt-Ergo 1.30, CVC4 1.5 and Z3 4.5.0
were detected by the \verb|why3 config --detect| command
\begin{description}
\item[Split] is bound to the 1-line strategy
......@@ -650,16 +650,26 @@ were detected by the \verb|why3 config --detect| command
t split_goal_wp exit
\end{verbatim}
\item[Auto level 0] is bound to
\begin{verbatim}
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
\end{verbatim}
The three provers are tried for a time limit of 1 second and memory
limit of 1~Gb, each in turn. This is a perfect strategy for a first
attempt to discharge a new goal.
\item[Auto level 1] is bound to
\begin{verbatim}
start:
c Z3,4.4.1, 1 1000
c Alt-Ergo,1.01, 1 1000
c CVC4,1.4, 1 1000
c Z3,4.5.0, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
t split_goal_wp start
c Z3,4.4.1, 10 4000
c Alt-Ergo,1.01, 10 4000
c CVC4,1.4, 10 4000
c Z3,4.5.0, 10 4000
c Alt-Ergo,1.30, 10 4000
c CVC4,1.5, 10 4000
\end{verbatim}
The three provers are first tried for a time limit of 1 second and
memory limit of 1~Gb, each in turn. If none of them succeed, a
......@@ -670,17 +680,17 @@ c CVC4,1.4, 10 4000
\item[Auto level 2] is bound to
\begin{verbatim}
start:
c Z3,4.4.1, 1 1000
c Eprover,1.8-001, 1 1000
c Z3,4.5.0, 1 1000
c Eprover,2.0, 1 1000
c Spass,3.7, 1 1000
c Alt-Ergo,1.01, 1 1000
c CVC4,1.4, 1 1000
c Alt-Ergo,1.30, 1 1000
c CVC4,1.5, 1 1000
t split_goal_wp start
c Z3,4.4.1, 5 2000
c Eprover,1.8-001, 5 2000
c Z3,4.5.0, 5 2000
c Eprover,2.0, 5 2000
c Spass,3.7, 5 2000
c Alt-Ergo,1.01, 5 2000
c CVC4,1.4, 5 2000
c Alt-Ergo,1.30, 5 2000
c CVC4,1.5, 5 2000
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
......@@ -688,12 +698,11 @@ g trylongertime
afterinline:
t split_goal_wp start
trylongertime:
c Z3,4.4.1, 30 4000
c Eprover,1.8-001, 30 4000
c Z3,4.5.0, 30 4000
c Eprover,2.0, 30 4000
c Spass,3.7, 30 4000
c Alt-Ergo,1.01, 30 4000
c CVC4,1.4, 30 4000
c Alt-Ergo,1.30, 30 4000
c CVC4,1.5, 30 4000
\end{verbatim}
Notice that now 5 provers are used. The provers are first tried for
a time limit of 1 second and memory limit of 1~Gb, each in turn. If
......@@ -701,7 +710,7 @@ c CVC4,1.4, 30 4000
the same strategy is retried on each sub-goals. If the split does
not succeed, the prover are tried again with limits of 5 s and 2
Gb. If all fail, we attempt the transformation of introduction of
premises in the context, followed by an inlining of the definiiions
premises in the context, followed by an inlining of the definitions
in the goals. We then attempt a split again, if the split succeeds,
we restart from the beginning, if it fails then provers are tried
again with 30s and 4 Gb.
......
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