Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Dafny: allow "_" as don't-care variable name | Unknown | 2012-08-30 |
| | |||
* | Dafny: support opening modules into the local scope | Jason Koenig | 2012-07-30 |
| | |||
* | Dafny: removed allocated, changed semantics of fresh | Jason Koenig | 2012-07-29 |
| | | | | | -allocated(x) removed, as really only useful in old(...) -old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype). | ||
* | Merge | Rustan Leino | 2012-07-09 |
|\ | |||
* | | Dafny: More work on the coinduction principle | Rustan Leino | 2012-07-09 |
| | | |||
| * | Dafny: added named expressions and replacement | Jason Koenig | 2012-07-09 |
| | | |||
* | | Dafny: added copredicates | Rustan Leino | 2012-07-03 |
|/ | |||
* | Dafny: fixed up test suite (temporarily removed autocontract tests) | Jason Koenig | 2012-06-28 |
| | |||
* | Dafny: Merge | Jason Koenig | 2012-06-27 |
|\ | |||
* | | Dafny: Fixed module bugs | Jason Koenig | 2012-06-27 |
| | | |||
* | | Dafny: Implemented abstract modules | Jason Koenig | 2012-06-26 |
| | | |||
| * | Dafny: allow "assume ..." as a refining statement (provided it replaces an ↵ | Unknown | 2012-06-22 |
| | | | | | | | | "assume E") | ||
| * | Dafny: Since it's no longer true that all types support equality at run-time ↵ | Unknown | 2012-06-21 |
|/ | | | | (in particular, codatatypes), Dafny needs to check this. In these changes, Dafny supports the "(==)" suffix to type parameters, infers that suffix in some cases, and enforces equality support in many places. Refinement and datatypes still need more attention in the Dafny implementation. | ||
* | Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to ↵ | Unknown | 2012-06-13 |
| | | | | check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P". | ||
* | Dafny: removed support for the old keyword "unlimited" (all functions are ↵ | Unknown | 2012-06-11 |
| | | | | limited) | ||
* | Dafny: change labels to use a generic singly linked list | Jason Koenig | 2012-06-06 |
| | |||
* | Dafny: Added map comprehensions and updated display syntax | Unknown | 2012-05-31 |
| | |||
* | Dafny: fixed minor map related issues | Unknown | 2012-05-29 |
| | |||
* | Dafny: fixed resolution bug for inductive datatypes (previous check did not ↵ | Unknown | 2012-04-25 |
| | | | | | | | handle generic datatypes correctly) Dafny: fixed compiler bug in inductive datatypes (missing type parameters in emitted code) Dafny: added "codatatype" declaration (syntax only for now) | ||
* | Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr; | Unknown | 2012-03-15 |
| | |||
* | Dafny: allow more skeleton statements in refinements | Unknown | 2012-03-02 |
| | |||
* | Dafny: added syntactic support for ...'s in statements, and started ↵ | Unknown | 2012-02-18 |
| | | | | implementation of refinement transformations thereof | ||
* | Dafny: allow signatures to be omitted on refining functions/methods | Unknown | 2012-02-16 |
| | |||
* | Dafny: Fixed a bug in the printing of let expressions. | wuestholz | 2012-01-24 |
| | |||
* | Dafny: allow parallel statements with an empty list of bound variables | Rustan Leino | 2012-01-17 |
| | |||
* | Dafny: allow definitions and uses of parameter-less predicates to go without ↵ | Rustan Leino | 2012-01-10 |
| | | | | parentheses | ||
* | 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: Fixed a bug in the pretty printer. | wuestholz | 2011-12-26 |
| | |||
* | Dafny: Extended the support for attributes on method/constructor calls. | wuestholz | 2011-12-23 |
| | |||
* | Dafny: Added support for attributes on method/constructor calls. | wuestholz | 2011-12-21 |
| | |||
* | Dafny: Added support for attributes on various specification constructs ↵ | wuestholz | 2011-12-07 |
| | | | | (assert, ensures, modifies, decreases, invariant). | ||
* | Dafny: Added "type" declaration (syntax: "type X;"), which introduces an ↵ | Rustan Leino | 2011-11-21 |
| | | | | arbitrary type (like a global type parameter). In the future, a refined module may allow such types to be instantiated. | ||
* | Dafny: added let expressions (syntax: "var x := E0; E1") | Rustan Leino | 2011-11-14 |
| | | | | | Dafny: firmed up semantics of assert/assume expressions (the condition is now good for all program control paths that pass through the expression) Dafny: various implementation clean-ups | ||
* | Dafny: added assert/assume expressions | Rustan Leino | 2011-11-09 |
| | |||
* | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" ↵ | Rustan Leino | 2011-10-26 |
| | | | | statement) | ||
* | Dafny: changed triggers (which are never really used, anyhow) from having a ↵ | Rustan Leino | 2011-10-21 |
| | | | | | | | special syntactic form to being just an attribute Dafny: added "parallel" statement (so far, only parsing and resolving) Dafny: allow types on bound variables in "match" expressions/statements (there's never any incentive to list them explicitly in the program text, but it nevertheless seemed silly to forbid them) | ||
* | Dafny: Added a 'Checked' configuration and fixed some runtime assertion ↵ | wuestholz | 2011-09-23 |
| | | | | violations. | ||
* | Dafny: Fixed a bug in the printer that led to a stack overflow. | wuestholz | 2011-08-11 |
| | |||
* | Merge | Jason Koenig | 2011-07-15 |
|\ | |||
| * | Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed ↵ | wuestholz | 2011-07-15 |
| | | | | | | | | some trailing whitespace. | ||
* | | Merge | Jason Koenig | 2011-07-14 |
|\| | |||
* | | Fixed printing of multisets. | Jason Koenig | 2011-07-11 |
| | | |||
| * | Dafny: allow constructors only inside classes, removed semi-colons at end of ↵ | Rustan Leino | 2011-07-11 |
| | | | | | | | | body-less functions/methods | ||
* | | Partial implementation of multisets. | Jason Koenig | 2011-07-11 |
|/ | |||
* | Added returns with parameters to printer. | Jason Koenig | 2011-06-29 |
| | |||
* | Initial modifies on loops implementation. Still some errors remaining. | Jason Koenig | 2011-06-28 |
| | |||
* | Dafny: added implicit datatype query fields and datatype destructor fields | Rustan Leino | 2011-06-05 |
| | |||
* | Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;" | Rustan Leino | 2011-05-28 |
| |