| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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")
|
| | |
|
| |
|
|
|
| |
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)
|
| |
|
|
| |
around the bound variables optional.
|
| |
|
|
| |
removed a level of directories for the Dafny VIM mode
|
| |
|
|
| |
renamed "ghost module" to "abstract module", adding a keyword "abstract"
|
| |
|
|
|
|
|
| |
* 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
|
| |\ |
|
| | |
| |
| |
| | |
and refining), no compilation or verification
|
| |/ |
|
| | |
|
| |
|
|
| |
keyword is parsed but ignored.
|
| |
|
|
| |
parallel syntax, other minor fixes
|
| | |
|
| |
|
|
|
|
|
| |
handle generic datatypes correctly)
Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code)
Dafny: added "codatatype" declaration (syntax only for now)
|
| | |
|
| | |
|
| |
|
|
| |
arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated.
|
| | |
|
| |
|
|
| |
statement)
|
| |
|
|
|
|
|
| |
special syntactic form to being just an attribute
Dafny: added "parallel" statement (so far, only parsing and resolving)
Dafny: allow types on bound variables in "match" expressions/statements (there's never any incentive to list them explicitly in the program text, but it nevertheless seemed silly to forbid them)
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Big change: Add type and allocatedness information everywhere in the Boogie translation. This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program. On the downside, it also requires discharging more antecedents in order to use some axioms. Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case).
* Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms). (Internally, this uses the new canCall mechanism.)
* Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type.
* More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal")
* Add axioms about idempotence of set union and intersection
* The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one
* In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase
* Fixed error in translation of while(*)
|
| |
|
|
|
|
| |
* Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation)
* Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays.
* Internally, this meant adding support for built-in classes and readonly fields
|
| |
|
|
| |
implementations in the refinement VC
|
| |
|
|
|
| |
* changed rule about scoping of out-parameters
* added "refines", "replaces", and "by" as keywords in emacs, vim, and latex style files
|
| | |
|
| |
|
qunyanm
Michael Lowell Roberts
Reza Ahmadi
Dan Rosén
Bryan Parno
Rustan Leino
Nadia Polikarpova
Unknown