summaryrefslogtreecommitdiff
path: root/Source/Dafny/Parser.cs
Commit message (Collapse)AuthorAge
* added trait feature:Gravatar Reza Ahmadi2014-07-18
| | | | | | -possibility to declare traits in Dafny -possibility to extend a class by a trait -possibility to override body-less methods
* Renamed "arbitrary type" to "opaque type"Gravatar Rustan Leino2014-07-15
|
* Support for type synonyms in refinementsGravatar Rustan Leino2014-07-14
| | | | Started allowing arbitrary types to have type parameters
* Added type synonyms. (No support yet for these in refinements.)Gravatar Rustan Leino2014-07-11
|
* MergeGravatar Rustan Leino2014-07-08
|\
* | Implemented compilation of the int<->real conversions, and changed the ↵Gravatar Rustan Leino2014-07-08
| | | | | | | | | | | | resolution and verification implementations of these. Changed FreshExpr to be a UnaryExpr, and also introduced the UnaryOpExpr subclass.
| * Allow array-type parameters to be filled in automatically.Gravatar leino2014-07-02
|/ | | | Enhanced filling in of datatype parameters: allow places that need only a prefix of the parameters of the datatype
* Added tuples and tuple types. Syntax is the expected one, namely parentheses ↵Gravatar Rustan Leino2014-06-27
| | | | around a comma-delimited list of expressions or types. Unit and the unit type are denoted ().
* Make syntax of "match" expressions and "match" statements the same -- curly ↵Gravatar Rustan Leino2014-06-24
| | | | braces around the cases are now supported for both and are optional for both
* Added support for 'dirty' forall statements.Gravatar chmaria2014-06-03
| | | | | | | | | | | 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.
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Members included from different files are now internally marked with an ↵Gravatar Rustan Leino2014-04-19
| | | | | | | IncludeToken; the previous scheme of using {:verify false} is no longer used. This makes "include" work with refinement features. Filenames of included files used in error messages are now what the user wrote, rather than absolute paths (which not only don't look so good, but are also problematic in comparing test output on different machines). Added dafny0/Includee.dfy to the test suite as well -- might as well include it, too, to get checked.
* MergeGravatar Rustan Leino2014-04-04
|\
* | Fixed refinement of modify statementsGravatar Rustan Leino2014-04-04
| |
| * Partial support for slicing a sequence using lengths, rather than indices.Gravatar Bryan Parno2014-04-04
|/ | | | Will get cleaner once we have tuple support.
* Added "modify Frame { Body }" statement.Gravatar Rustan Leino2014-04-04
|
* Added "modify" statement.Gravatar Rustan Leino2014-04-03
| | | | In a frame govered by a ghost context, ignore explicit mentions of `g if g is a ghost field.
* Auto-set type arguments of built-in collection types, just like for ↵Gravatar Rustan Leino2014-03-21
| | | | user-defined types.
* Fixed resolution bug where "var x := x" was allowed.Gravatar Rustan Leino2014-03-17
|
* Refactoring: renamed VarDecl to LocalVariable, and renamed VarDeclStmt.Lhss ↵Gravatar Rustan Leino2014-03-17
| | | | to VarDeclStmt.Locals
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵Gravatar Rustan Leino2014-02-23
| | | | -> "prefix lemma")
* Allow unary minus on realsGravatar Rustan Leino2014-02-13
|
* Fixed crash in parserGravatar Rustan Leino2014-02-13
|
* Preliminary support for reals in Dafny specs. No compiler suport yet.Gravatar Bryan Parno2014-02-10
|
* Produce hover text for many of the refinement omissions (i.e., "..." and the ↵Gravatar Rustan Leino2014-01-31
| | | | like).
* Allow left-hand sides of a let expression to be patterns (like in the case ↵Gravatar Rustan Leino2014-01-08
| | | | | | | 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.
* Added ghost let expressions.Gravatar Rustan Leino2014-01-05
|
* Make ModuleDefinition inherit from TopLevelDecl instead of just DeclarationGravatar Bryan Parno2014-01-03
|
* MergeGravatar Rustan Leino2013-12-30
|\
* | Added proper parsing for StmtExpr's in all contexts.Gravatar Rustan Leino2013-12-30
| | | | | | | | | | | | Adjusted printer accordingly. Fixed bug in Substituter for CalcStmt in StmtExpr's. Always show terminating semi-colon in hover-text for default decreases clauses.
| * Changed the iterator class hover text back to the iterator name (which is ↵Gravatar Rustan Leino2013-12-20
|/ | | | consistent with everything else), not the "iterator" keyword
* Added an .EndTok for every statement. (Note, in some places, especially in ↵Gravatar Rustan Leino2013-12-19
| | | | | | | VarDecl statements, there's often no good .EndTok information.) Used the .EndTok in CaptureState information. In other words, move the blue dots in the IDE to after the statement just executed. Removed /*!*/ comments in some parts of the source code -- CodeContracts reveal this information.
* Fixed pretty printing of calc statements to use the new(-since-long) format.Gravatar Rustan Leino2013-12-17
| | | | | Disallow dangling operator in calc (which had also allowed soundness bug). Don't reprove the test files in dafny0 after testing their pretty printing.
* Add support for the :axiom attribute for ghost methods.Gravatar Bryan Parno2013-12-13
| | | | | | This suppresses compiler errors for ghost methods and functions without bodies. Also changed the parser to complain about bodyless methods and functions without bodies if /noCheating:1 is specified.
* Add support for the "include" keyword, which accepts a (possibly relative) pathGravatar Bryan Parno2013-12-10
| | | | | 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.
* Added support for attributes on variable declarations.Gravatar wuestholz2013-11-18
|
* Allow calls to side-effect-free ghost methods from expressionsGravatar Rustan Leino2013-08-06
|
* Merged PredicateExpr and CalcExpr into a single StmtExprGravatar Rustan Leino2013-08-06
| | | | In that process, added a SubstStmt method (and entourage) for substituting into statements
* Introduced keywords "lemma" (like a "ghost method", but not allowed to have ↵Gravatar Rustan Leino2013-08-02
| | | | a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point)
* Regenerated Parser after a merge.Gravatar Nadia Polikarpova2013-07-31
|
* Add support for hexidecimal numbers.Gravatar parno2013-07-30
|
* Fixed build failure.Gravatar wuestholz2013-07-25
|
* Allow field names to be sequences of digits (this is nice, for example, to ↵Gravatar Rustan Leino2013-07-24
| | | | define a Tuple with fields .0 and .1)
* Because of neighboring parse conflict handlers, must call ResetPeek()Gravatar Rustan Leino2013-07-10
|
* Fixed parsing bug in "if" and "while" guardsGravatar Rustan Leino2013-07-10
|
* Made the semi-colon after "type" and "module" declarations optional.Gravatar Rustan Leino2013-05-10
|
* Make semi-colon after datatype/codatatype declaration optional (in the ↵Gravatar Rustan Leino2013-04-19
| | | | future, it will not be allowed at all)
* The "choose" statement, hacky and specialized as it was, is now gone. Use ↵Gravatar Rustan Leino2013-03-27
| | | | the assign-such-that statement instead. For example: x :| x in S;
* Finished support for ==# in calc, changed Paulson example to use it.Gravatar Nadia Polikarpova2013-03-20
|
* Added explies support to calculations.Gravatar Nadia Polikarpova2013-03-15
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 06:52:38 +0000