| Commit message (Collapse) | Author | Age |
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
t<i> op t<i + 1>), generated during resolution; first version of the translation
|
|\ |
|
| | |
|
| | |
|
| | |
|
| | |
|
|/
|
|
| |
and axiomatize [][..0] == [] == [][0..]
|
|
|
|
| |
refinements (things like multiple labels are still not thought through very well)
|
| |
|
|\ |
|
| |
| |
| |
| | |
tail-recursive methods
|
| |
| |
| |
| | |
optional "tailrecursion" attribute). Also, let the cloner also clone attributes.
|
| |
| |
| |
| | |
an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be
|
| |
| |
| |
| | |
as an identifier definition)
|
| | |
|
|/ |
|
|
|
|
| |
result the function itself
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
DafnyExtension: added hover text for identifiers
|
|
|
|
| |
crashing after certain deletes)
|
| |
|
| |
|
|
|
|
| |
locations, set a 10-second timeout
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| | |
visually indicates a non-verified buffer
|
|/ |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
keyword is parsed but ignored.
|
|
|
|
|
| |
-allocated(x) removed, as really only useful in old(...)
-old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype).
|
| |
|
| |
|
|
|
|
| |
parallel statements.
|
|
|
|
|
|
|
| |
module A as B = C)
* * *
Dafny: compilation of abstract modules, including local definitions (as in module A as B = C)
|