Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Allow custom operators on a line | 2012-09-17 | |
| | |||
* | Allow several calculation operators (for the whole calculation) | 2012-09-16 | |
| | |||
* | Renamed terms into lines (according to the proposal), fixed some contracts | 2012-09-16 | |
| | |||
* | Calc statements: Renamed Steps into Terms; introduced Steps (expressions ↵ | 2012-09-14 | |
| | | | | t<i> op t<i + 1>), generated during resolution; first version of the translation | ||
* | Pretty-print calc statements | 2012-09-14 | |
| | |||
* | Dafny: allow "_" as don't-care variable name | 2012-08-30 | |
| | |||
* | Dafny: support opening modules into the local scope | 2012-07-30 | |
| | |||
* | Dafny: removed allocated, changed semantics of fresh | 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 | 2012-07-09 | |
|\ | |||
* | | Dafny: More work on the coinduction principle | 2012-07-09 | |
| | | |||
| * | Dafny: added named expressions and replacement | 2012-07-09 | |
| | | |||
* | | Dafny: added copredicates | 2012-07-03 | |
|/ | |||
* | Dafny: fixed up test suite (temporarily removed autocontract tests) | 2012-06-28 | |
| | |||
* | Dafny: Merge | 2012-06-27 | |
|\ | |||
* | | Dafny: Fixed module bugs | 2012-06-27 | |
| | | |||
* | | Dafny: Implemented abstract modules | 2012-06-26 | |
| | | |||
| * | Dafny: allow "assume ..." as a refining statement (provided it replaces an ↵ | 2012-06-22 | |
| | | | | | | | | "assume E") | ||
| * | Dafny: Since it's no longer true that all types support equality at run-time ↵ | 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 ↵ | 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 ↵ | 2012-06-11 | |
| | | | | limited) | ||
* | Dafny: change labels to use a generic singly linked list | 2012-06-06 | |
| | |||
* | Dafny: Added map comprehensions and updated display syntax | 2012-05-31 | |
| | |||
* | Dafny: fixed minor map related issues | 2012-05-29 | |
| | |||
* | Dafny: fixed resolution bug for inductive datatypes (previous check did not ↵ | 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; | 2012-03-15 | |
| | |||
* | Dafny: allow more skeleton statements in refinements | 2012-03-02 | |
| | |||
* | Dafny: added syntactic support for ...'s in statements, and started ↵ | 2012-02-18 | |
| | | | | implementation of refinement transformations thereof | ||
* | Dafny: allow signatures to be omitted on refining functions/methods | 2012-02-16 | |
| | |||
* | Dafny: Fixed a bug in the printing of let expressions. | 2012-01-24 | |
| | |||
* | Dafny: allow parallel statements with an empty list of bound variables | 2012-01-17 | |
| | |||
* | Dafny: allow definitions and uses of parameter-less predicates to go without ↵ | 2012-01-10 | |
| | | | | parentheses | ||
* | Dafny: added predicates | 2012-01-10 | |
| | |||
* | Dafny: firmed up the module system | 2012-01-05 | |
| | |||
* | Dafny: Start of new refinement features -- clean out old ones | 2012-01-04 | |
| | |||
* | Dafny: Fixed a bug in the pretty printer. | 2011-12-26 | |
| | |||
* | Dafny: Extended the support for attributes on method/constructor calls. | 2011-12-23 | |
| | |||
* | Dafny: Added support for attributes on method/constructor calls. | 2011-12-21 | |
| | |||
* | Dafny: Added support for attributes on various specification constructs ↵ | 2011-12-07 | |
| | | | | (assert, ensures, modifies, decreases, invariant). | ||
* | Dafny: Added "type" declaration (syntax: "type X;"), which introduces an ↵ | 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") | 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 | 2011-11-09 | |
| | |||
* | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" ↵ | 2011-10-26 | |
| | | | | statement) | ||
* | Dafny: changed triggers (which are never really used, anyhow) from having a ↵ | 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 ↵ | 2011-09-23 | |
| | | | | violations. | ||
* | Dafny: Fixed a bug in the printer that led to a stack overflow. | 2011-08-11 | |
| | |||
* | Merge | 2011-07-15 | |
|\ | |||
| * | Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed ↵ | 2011-07-15 | |
| | | | | | | | | some trailing whitespace. | ||
* | | Merge | 2011-07-14 | |
|\| | |||
* | | Fixed printing of multisets. | 2011-07-11 | |
| | | |||
| * | Dafny: allow constructors only inside classes, removed semi-colons at end of ↵ | 2011-07-11 | |
| | | | | | | | | body-less functions/methods |