Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵ | Rustan Leino | 2014-02-23 |
| | | | | -> "prefix lemma") | ||
* | Allow unary minus on reals | Rustan Leino | 2014-02-13 |
| | |||
* | Fixed crash in parser | Rustan Leino | 2014-02-13 |
| | |||
* | Preliminary support for reals in Dafny specs. No compiler suport yet. | Bryan Parno | 2014-02-10 |
| | |||
* | Produce hover text for many of the refinement omissions (i.e., "..." and the ↵ | Rustan Leino | 2014-01-31 |
| | | | | like). | ||
* | Allow left-hand sides of a let expression to be patterns (like in the case ↵ | Rustan Leino | 2014-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. | Rustan Leino | 2014-01-05 |
| | |||
* | Make ModuleDefinition inherit from TopLevelDecl instead of just Declaration | Bryan Parno | 2014-01-03 |
| | |||
* | Merge | Rustan Leino | 2013-12-30 |
|\ | |||
* | | Added proper parsing for StmtExpr's in all contexts. | Rustan Leino | 2013-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 ↵ | Rustan Leino | 2013-12-20 |
|/ | | | | consistent with everything else), not the "iterator" keyword | ||
* | Added an .EndTok for every statement. (Note, in some places, especially in ↵ | Rustan Leino | 2013-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. | Rustan Leino | 2013-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. | Bryan Parno | 2013-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) path | Bryan Parno | 2013-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. | wuestholz | 2013-11-18 |
| | |||
* | Allow calls to side-effect-free ghost methods from expressions | Rustan Leino | 2013-08-06 |
| | |||
* | Merged PredicateExpr and CalcExpr into a single StmtExpr | Rustan Leino | 2013-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 ↵ | Rustan Leino | 2013-08-02 |
| | | | | a "modifies" clause) and "colemma" (synonymous with "comethod"; perhaps "comethod" will go away at some point) | ||
* | Regenerated Parser after a merge. | Nadia Polikarpova | 2013-07-31 |
| | |||
* | Add support for hexidecimal numbers. | parno | 2013-07-30 |
| | |||
* | Fixed build failure. | wuestholz | 2013-07-25 |
| | |||
* | Allow field names to be sequences of digits (this is nice, for example, to ↵ | Rustan Leino | 2013-07-24 |
| | | | | define a Tuple with fields .0 and .1) | ||
* | Because of neighboring parse conflict handlers, must call ResetPeek() | Rustan Leino | 2013-07-10 |
| | |||
* | Fixed parsing bug in "if" and "while" guards | Rustan Leino | 2013-07-10 |
| | |||
* | Made the semi-colon after "type" and "module" declarations optional. | Rustan Leino | 2013-05-10 |
| | |||
* | Make semi-colon after datatype/codatatype declaration optional (in the ↵ | Rustan Leino | 2013-04-19 |
| | | | | future, it will not be allowed at all) | ||
* | The "choose" statement, hacky and specialized as it was, is now gone. Use ↵ | Rustan Leino | 2013-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. | Nadia Polikarpova | 2013-03-20 |
| | |||
* | Added explies support to calculations. | Nadia Polikarpova | 2013-03-15 |
| | |||
* | Added the <== operator. | Nadia Polikarpova | 2013-03-14 |
| | |||
* | Renamed "parallel" statement to "forall" statement, and made the parentheses ↵ | Rustan Leino | 2013-03-06 |
| | | | | around the bound variables optional. | ||
* | Support for paren-free guards in if and while statements. | Nadia Polikarpova | 2013-02-15 |
| | |||
* | First take on calc expressions. | Nadia Polikarpova | 2013-02-14 |
| | |||
* | Changed calc syntax (custom operators are now written before the hint) | Nadia Polikarpova | 2013-02-08 |
| | |||
* | "!!" can now be parsed as two "!". More concise parsing for "!in". | Nadia Polikarpova | 2013-02-07 |
| | |||
* | Added parsing and resolution of a new let-such-that expression. Translation ↵ | Rustan Leino | 2013-01-21 |
| | | | | has yet to be implemented. | ||
* | Added some co- test cases. Fixed some bugs. | Rustan Leino | 2013-01-20 |
| | |||
* | Removed the syntactic form copredicate #-form with the implicit argument. | Rustan Leino | 2013-01-16 |
| | | | | Added syntactic support for codatatype #-form equalities. | ||
* | Improved error message for making the mistake of saying 'returns' instead of ↵ | Rustan Leino | 2012-11-25 |
| | | | | 'yields' for an iterator | ||
* | Parse prefix predicates/methods | Rustan Leino | 2012-11-24 |
| | |||
* | renamed "abstract module" to "module facade" | Rustan Leino | 2012-10-22 |
| | | | | renamed "ghost module" to "abstract module", adding a keyword "abstract" | ||
* | New feature: | Rustan Leino | 2012-10-11 |
| | | | | | | | * 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 | ||
* | Support default (which, here, means nameless) class-instance constructors | Rustan Leino | 2012-10-05 |
| | |||
* | Put all sources under \Source directory | Rustan Leino | 2012-10-04 |