| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
half a second, but delay calling Dafny resolver until the text buffer hasn't
been changed for 5 seconds. Also save the parsing result from TokenTagger in
ITextBuffer's property instead of in a static field.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
- cache scan results so it can be shared between different instances of
DafnyTokenTagger
- Instead of rescanning the whole text buffer upon a text change, only rescan
the text span that the text change is in.
- set the timer to half a second to match the comment at the beginnig of
the file. The event change are only passed along to Dafny when the user stop
typing for half a second.
- Change framework dependence so the project can work with version 4.5 and
higher.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings.
Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions.
Fixed lack of operator resolution in custom attributes.
|
| |
|
|
| |
Added parsing of constraints (beyond parsing is yet to come)
|
| |
|
|
|
|
| |
-possibility to declare traits in Dafny
-possibility to extend a class by a trait
-possibility to override body-less methods
|
| | |
|
| | |
|
| |
|
|
| |
In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
|
| | |
|
| |
|
|
| |
-> "prefix lemma")
|
| | |
|
| |
|
|
|
|
| |
Translator had not been run).
Fixed duplicate hover text information for Lines of calc statements.
|
| |
|
|
|
| |
to another Dafny file. That file's functions and methods are included but not checked.
This is intended to support incremental verification on a per-file basis.
|
| | |
|
| |
|
|
| |
a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
|
| |
|
|
| |
state.
|
| |
|
|
| |
text.
|
| |
|
|
| |
resolution and displaying it.
|
| | |
|
| | |
|
| |
|
|
| |
around the bound variables optional.
|
| |
|
|
|
| |
Remove some duplicated hover text in DafnyExtension
Enable Code Contracts in the build
|
| |
|
|
| |
removed a level of directories for the Dafny VIM mode
|
| |
|
|
| |
renamed "ghost module" to "abstract module", adding a keyword "abstract"
|
| |
|
|
|
|
| |
re-verifying the postcondition at that time
let refined classes inherit attributes
|
| |
|
|
|
|
|
| |
* Added "comethod" declarations and support for writing manual co-inductive proofs (but currently blindly assume comethod postconditions to, in positive positions, only have copredicates and codatatype equalities--other cases still need to be dealt with)
Code restructuring:
* New set of Boogie procedure stubs generated for each other
* Start of improvements around TrSplitExpr
|
| |
|
qunyanm
Reza Ahmadi
Bryan Parno
Rustan Leino