Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
why3
Project
Project
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
87
Issues
87
List
Boards
Labels
Milestones
Merge Requests
9
Merge Requests
9
Packages
Packages
Container Registry
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Commits
Issue Boards
Open sidebar
Why3
why3
Commits
f82e91b3
Commit
f82e91b3
authored
Mar 14, 2018
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Beautify changes.
parent
135b6982
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
47 additions
and
37 deletions
+47
-37
CHANGES.md
CHANGES.md
+42
-36
doc/manual.tex
doc/manual.tex
+5
-1
No files found.
CHANGES.md
View file @
f82e91b3
:x: marks a potential source of incompatibility
x syntax changes for programs; good luck!
*
let function / let predicate / val function / val predicate
introduce symbols in both logic and programs
*
overloading of program symbols
*
no more "self" in type invariants
x new clause "alias" in function contracts
x logical symbols can only be used in ghost code
x no more polymorphic equality in programs
equality functions must be declared/defined on per type basis
(this is already done for type int in the standard library)
x type invariants produce logical axioms
*
a type with an invariant must be proved to be inhabited
*
local exceptions; break, continue, and return statements
*
match with exceptions
*
"for" loop on range types (including machine integers from the library)
x no more "loop" statement (use "while true" instead)
*
vc:sp switches from traditional WP to Flanagan-Saxe-like VCgen,
on per expression basis
*
type coercions in logic
*
new extraction to OCaml
*
new extraction to C
*
.why extension is now deprecated; use .mlw instead
*
"theory" now deprecated; use "module" instead
Core
*
improved support of counter-examples
Language
*
numerous changes to syntax, see documentation appendix :x:
*
`let function`
,
`let predicate`
,
`val function`
, and
`val predicate`
introduce symbols in both logic and programs
*
logical symbols can no longer be used in non-ghost code;
in particular, there is no polymorphic equality in programs any more,
so equality functions must be declared/defined on a per-type basis
(already done for type
`int`
in the standard library) :x:
*
added overloading of program symbols
*
new clause
`alias`
in function contracts :x:
*
support for multiple assignments
*
type invariants now produce logical axioms;
a type with an invariant must be proved to be inhabited :x:
*
support for local exceptions using
`exception ... in ...`
*
added
`break`
,
`continue`
, and
`return`
statements
*
support for
`exception`
branches in
`match`
constructs
*
support for
`for`
loops on range types
(including machine integers from the standard library)
*
attribute
`[@vc:sp]`
on an expression switches from traditional WP to
Flanagan-Saxe-like VC generation
*
support for type coercions in logic using
`meta coercion`
*
deprecated
`theory`
; use
`module`
instead
Extraction
*
improved extraction to OCaml
*
added partial extraction to C
Transformations
*
transformations can now have arguments
*
new transformations assert, apply, cut, rewrite, ...
à la Coq
*
new
transformations for reflection-based proofs
*
added transformations
`assert`
,
`apply`
,
`cut`
,
`rewrite`
, etc,
à la Coq
*
added
transformations for reflection-based proofs
Drivers
*
"use" is allowed
*
support for
`use`
in theory drivers
*
counterexamples
*
new IDE
IDE
*
source is now editable
*
CLI to call transformations and provers
*
premises are no longer implicitly introduced
*
command-line interface to call transformations and provers
*
new input format for (a small subset of) Python
*
the "why3" Coq tactic is now deprecated
Tools
*
deprecated
`.why`
file extension; use
`.mlw`
instead
Provers
*
deprecated the
`why3`
Coq tactic
Version 0.88.3, January 11, 2018
--------------------------------
...
...
@@ -112,6 +115,9 @@ User features
floating-point values, support for Z3 in addition to CVC4.
More details in the manual, section 6.3.5 "Displaying Counterexamples".
Plugins
*
new input format for a small subset of Python
Provers
*
support for Isabelle 2017 (released Oct 2017)
*
discarded support for Isabelle 2016 (2016-1 still supported) :x:
...
...
doc/manual.tex
View file @
f82e91b3
...
...
@@ -301,7 +301,7 @@ egalite sur les type algebriques ? engendrees automatiquement ?
\hline
\texttt
{
assert
\{
... (old x) ...
\}
}
&
\texttt
{
assert
\{
... (x at Init) ...
\}
}
\\
\hline
\texttt
{
\char
`
\\
x
{
.
}
e
}
&
\texttt
{
fun x -> e
}
\\
\texttt
{
\char
`
\\
x
.
e
}
&
\texttt
{
fun x -> e
}
\\
\hline
\texttt
{
use HighOrd
}
&
nothing, not needed anymore
\\
\hline
...
...
@@ -317,6 +317,10 @@ egalite sur les type algebriques ? engendrees automatiquement ?
\hline
\texttt
{
meta M prop P
}
&
\texttt
{
meta M lemma P
}
or
\texttt
{
meta M axiom P
}
or
\texttt
{
meta M goal P
}
\\
\hline
\texttt
{
loop ... end
}
&
\texttt
{
while true do ... done
}
\\
\hline
\texttt
{
type ... invariant
\{
... self.foo ...
\}
}
&
\texttt
{
type ... invariant
\{
... foo ...
\}
}
\\
\hline
\end{tabular}
\end{center}
...
...
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