| Commit message (Expand) | Author | Age |
* | Dafny: fixed a couple of compiler bugs | Rustan Leino | 2012-02-16 |
* | Dafny: fixed bug in compilation of let expressions. | Rustan Leino | 2012-01-26 |
* | Dafny: fixed bug in compilation of generic datatypes | Rustan Leino | 2012-01-18 |
* | Dafny: allow parallel statements with an empty list of bound variables | Rustan Leino | 2012-01-17 |
* | Dafny: some bug fixes | Rustan Leino | 2012-01-10 |
* | Dafny: Start of new refinement features -- clean out old ones | Rustan Leino | 2012-01-04 |
* | Dafny: compile let expressions efficiently (i.e., with an extra variable, not... | Rustan Leino | 2012-01-04 |
* | Dafny: compile to .exe only if there is a Main method; otherwise, compile to ... | Rustan Leino | 2011-12-19 |
* | Merge | Rustan Leino | 2011-12-07 |
|\ |
|
* | | Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable well... | wuestholz | 2011-12-07 |
| * | 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: added assert/assume expressions | Rustan Leino | 2011-11-09 |
* | Dafny induction: | Rustan Leino | 2011-10-29 |
* | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" s... | Rustan Leino | 2011-10-26 |
* | Dafny: removed support for assigning to an array-range (that is, an assignmen... | Rustan Leino | 2011-10-26 |
* | Dafny: implemented compilation of parallel statements | Rustan Leino | 2011-10-25 |
* | Dafny: changed triggers (which are never really used, anyhow) from having a s... | Rustan Leino | 2011-10-21 |
* | Merge | Rustan Leino | 2011-09-28 |
|\ |
|
| * | Dafny: Added some assertions. | wuestholz | 2011-09-23 |
* | | Dafny: generate a compiler error upon encountering an assume statement | Rustan Leino | 2011-09-11 |
* | | Dafny: fixed compilation bug (datatype equality had used pointer equality, no... | Rustan Leino | 2011-09-11 |
* | | Dafny: fixed compilation error where type of target "null" was undetermined | Rustan Leino | 2011-09-11 |
|/ |
|
* | Merge | Jason Koenig | 2011-07-15 |
|\ |
|
* | | Added compilation support for multisets and sequences from arrays. | Jason Koenig | 2011-07-15 |
| * | Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed so... | wuestholz | 2011-07-15 |
|/ |
|
* | Dafny: Dafny now uses the Euclidean definition of division. (Verifier and run... | Jason Koenig | 2011-07-08 |
* | Fixed bug in compiler relating to returns with parameters. | Jason Koenig | 2011-06-29 |
* | Initial implementation of return statments with parameters. | Jason Koenig | 2011-06-29 |
* | Dafny: better error message when "decreases *" is attempted on a function or ... | Rustan Leino | 2011-06-20 |
* | Dafny: added implicit datatype query fields and datatype destructor fields | Rustan Leino | 2011-06-05 |
* | Dafny: compiler fixes | Rustan Leino | 2011-05-31 |
* | Dafny: compile multi-assignments, compile calls with more general LHSs | Rustan Leino | 2011-05-31 |
* | Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;" | Rustan Leino | 2011-05-28 |
* | Dafny: fixed parsing bug that prevented all expressions from occurring in mat... | Rustan Leino | 2011-05-27 |
* | Dafny: fixed compilation bug that produced an extraneous comma in the target ... | Rustan Leino | 2011-05-27 |
* | Dafny: | 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: let verifier, not the resolver, check for missing cases in match expre... | Rustan Leino | 2011-05-19 |
* | Dafny: added set comprehension expressions | Rustan Leino | 2011-05-18 |
* | Dafny: added optional range expressions to logical quantifiers, preparing for... | Rustan Leino | 2011-05-15 |
* | Dafny: fixed compilation bugs, added @-signs in front of identifiers to avoid... | Rustan Leino | 2011-05-11 |
* | Dafny: Added support for an initializing call as part of the new-allocation s... | rustanleino | 2011-03-27 |
* | Dafny: added "choose" operator on sets | rustanleino | 2011-03-26 |
* | Dafny: compile quantifiers | rustanleino | 2011-03-26 |
* | Dafny: | rustanleino | 2011-02-17 |