| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
statements
|
|
|
|
| |
Disallow backslash from being part of identifier names.
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
Cleaner printing of .reads and .requires members of the built-in arrow "classes".
|
|
|
|
| |
along with a backward-compatibility warning message if such declarations are attempted
|
| |
|
| |
|
| |
|
|
|
|
| |
Fixed bug in type checking for integer division.
|
| |
|
|\ |
|
| |
| |
| |
| | |
and forall statements, and more expressions
|
| |\
| |/
|/| |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* The reads clause now needs to be self framing.
* The requires clause now needs to be framed by the reads clause.
* There are one-shot lambdas, with a single arrow, but they will probably be
removed.
* There is a {:heapQuantifier} attribute to quantifiers, but they will
probably be removed.
* Add smart handling of type variables
* Add < and > for datatype & type parameter
|
| | |
|
|/
|
|
|
|
| |
-possibility to declare traits in Dafny
-possibility to extend a class by a trait
-possibility to override body-less methods
|
| |
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| | |
resolution and verification implementations of these.
Changed FreshExpr to be a UnaryExpr, and also introduced the UnaryOpExpr subclass.
|
| |\
| |/
|/| |
|
| | |
|
| |
| |
| |
| | |
around a comma-delimited list of expressions or types. Unit and the unit type are denoted ().
|
| |
| |
| |
| | |
braces around the cases are now supported for both and are optional for both
|
|/
|
|
|
|
|
|
|
|
|
| |
One can now write forall statements without bodies
(but with ensures clauses) as follows:
forall s | s in S ensures s < 0;
where S is set<int>.
The ensures clauses are assumed but not checked.
|
|\ |
|
| |
| |
| |
| | |
refinement.
|
| | |
|
| |
| |
| |
| | |
In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
|
|/ |
|
|
|
|
| |
to VarDeclStmt.Locals
|
|
|
|
|
| |
Changed VarDecl to no longer inherit from Statement.
Removed ConcreteSyntaxStatement and changed VarDeclStmt's superclass be Statement.
|
|
|
|
| |
-> "prefix lemma")
|
| |
|
| |
|
| |
|
|
|
|
| |
like).
|
|\ |
|
| |
| |
| |
| |
| |
| |
| | |
of a match expression).
Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator.
Fixed compilation of match expressions, to allow them anywhere.
|
| |
| |
| |
| | |
Add better handling of resolved data types in autoReq.
|
|/
|
|
| |
:autoReq attribute.
|
|
|
|
| |
the top-level of function bodies. (Note, resolver also needs to allow this before the user can take advantage of this.)
|
|
|
|
|
|
| |
Adjusted printer accordingly.
Fixed bug in Substituter for CalcStmt in StmtExpr's.
Always show terminating semi-colon in hover-text for default decreases clauses.
|
|
|
|
| |
Make this information available as AdditionalInformation, that is, as hover text in the IDE.
|
|
|
|
|
| |
Disallow dangling operator in calc (which had also allowed soundness bug).
Don't reprove the test files in dafny0 after testing their pretty printing.
|
|\ |
|
| | |
|
|/
|
|
| |
are ghost
|
|
|
|
| |
In that process, added a SubstStmt method (and entourage) for substituting into statements
|