| Commit message (Expand) | Author | Age |
* | Dafny: removed allocated keyword, changed module import syntax. "opened" keyw... | Jason Koenig | 2012-07-30 |
* | Dafny: removed allocated, changed semantics of fresh | Jason Koenig | 2012-07-29 |
* | Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to ... | Jason Koenig | 2012-07-10 |
* | Dafny: rebuilt parser/scanner after previous merge | Rustan Leino | 2012-07-09 |
* | Dafny: added copredicates | Rustan Leino | 2012-07-03 |
* | Dafny: Merge | Jason Koenig | 2012-06-27 |
|\ |
|
* | | Dafny: Implemented abstract modules | Jason Koenig | 2012-06-26 |
| * | Dafny: Since it's no longer true that all types support equality at run-time ... | Unknown | 2012-06-21 |
|/ |
|
* | Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to c... | Unknown | 2012-06-13 |
* | Dafny: allow types to be qualified with the name of the module that declares ... | Unknown | 2012-06-11 |
* | Dafny: removed support for the old keyword "unlimited" (all functions are lim... | Unknown | 2012-06-11 |
* | Dafny: added finite maps | Unknown | 2012-05-25 |
* | Dafny: fixed resolution bug for inductive datatypes (previous check did not h... | Unknown | 2012-04-25 |
* | Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr; | Unknown | 2012-03-15 |
* | Dafny: added ghost modules (the meaning is simply that such a module will not... | Rustan Leino | 2012-03-07 |
* | Dafny: allow signatures to be omitted on refining functions/methods | Unknown | 2012-02-16 |
* | Dafny: re-ran parser generator to use latest .frame files | Rustan Leino | 2012-02-16 |
* | Dafny: added predicates | Rustan Leino | 2012-01-10 |
* | Dafny: firmed up the module system | Rustan Leino | 2012-01-05 |
* | Dafny: Start of new refinement features -- clean out old ones | Rustan Leino | 2012-01-04 |
* | Dafny: Added support for attributes on various specification constructs (asse... | wuestholz | 2011-12-07 |
* | Dafny: reran Coco on merged Dafny.atg | Rustan Leino | 2011-12-07 |
* | Merge | Rustan Leino | 2011-12-07 |
|\ |
|
* | | Dafny: Made some minor changes to the grammar. | wuestholz | 2011-12-06 |
| * | Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbi... | Rustan Leino | 2011-11-21 |
|/ |
|
* | Dafny: added let expressions (syntax: "var x := E0; E1") | Rustan Leino | 2011-11-14 |
* | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" s... | Rustan Leino | 2011-10-26 |
* | Dafny: changed triggers (which are never really used, anyhow) from having a s... | Rustan Leino | 2011-10-21 |
* | Dafny: fixed parsing bug with "!in" | Rustan Leino | 2011-09-08 |
* | Dafny: re-ran parser generator to include semicolon-less body-less functions/... | Rustan Leino | 2011-07-26 |
* | Multiset forming operators added. | Jason Koenig | 2011-07-11 |
* | Partial implementation of multisets. | Jason Koenig | 2011-07-11 |
* | Added loop modifies clause syntax. | Jason Koenig | 2011-06-23 |
* | Dafny: better error message when "decreases *" is attempted on a function or ... | Rustan Leino | 2011-06-20 |
* | Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;" | Rustan Leino | 2011-05-28 |
* | Dafny: added constructors | Rustan Leino | 2011-05-28 |
* | Dafny: fixed parsing bug that prevented all expressions from occurring in mat... | Rustan Leino | 2011-05-27 |
* | Dafny: permanently changed the syntax of "datatype" declarations to what prev... | Rustan Leino | 2011-05-27 |
* | Dafny: retired "use" statements | Rustan Leino | 2011-05-27 |
* | Dafny: retired the "call" keyword | Rustan Leino | 2011-05-26 |
* | Dafny: cleaned up parser, moved foreach statement from AssignStmt<> parsing t... | Rustan Leino | 2011-05-25 |
* | Dafny: changed local "var" introductions to use new VarDeclStmt instead of pa... | Rustan Leino | 2011-05-24 |
* | Dafny: | Rustan Leino | 2011-05-24 |
* | Dafny: | Rustan Leino | 2011-05-21 |
* | Dafny: added alternative statement and alternative-loop statement | Rustan Leino | 2011-05-19 |
* | Dafny: added set comprehension expressions | Rustan Leino | 2011-05-18 |
* | Dafny: fixed typo in parser code | Rustan Leino | 2011-05-13 |
* | Dafny: fixed bugs in resolution of multi-dimensional arrays | Rustan Leino | 2011-05-12 |
* | Dafny: Fix parsing of if-then-else expressions, and don't require parentheses... | Rustan Leino | 2011-04-21 |
* | Dafny: Alternative (and candidate replacement) syntax for declaring datatypes | Rustan Leino | 2011-04-20 |