Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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: added contracts to IRewriter methods | Unknown | 2012-06-22 |
| | | |||
| * | Dafny: allow "assume ..." as a refining statement (provided it replaces an ↵ | Unknown | 2012-06-22 |
| | | | | | | | | "assume E") | ||
| * | Dafny: deal with equality-support issues in refinements | Unknown | 2012-06-22 |
| | | | | | | | | Dafny: a small amount of refactoring and bug fixes | ||
| * | 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: improved refinement features; added staged version of the proof of ↵ | Unknown | 2012-06-19 |
|/ | | | | the Schorr-Waite algorithm (the staging features, as well as the newly added comments, make the verification much more digestible) | ||
* | 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: allow types to be qualified with the name of the module that declares ↵ | Unknown | 2012-06-11 |
| | | | | them (for now, this is supported only in type expressions and "new" allocations, not in places where the type name is used to qualify some other type member) | ||
* | Dafny: fixed bug in type cloning, as part of refinement machinery | Unknown | 2012-06-11 |
| | |||
* | 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: added finite maps | Unknown | 2012-05-25 |
| | |||
* | 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: support assign-such-that in var declarations in refinements | Unknown | 2012-03-15 |
| | |||
* | 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 ↵ | Rustan Leino | 2012-03-07 |
| | | | | | | | not be compiled) Dafny: improved :autocontracts heuristic for detecting "simple query method" Dafny: fixed some bugs | ||
* | Dafny: allow more skeleton statements in refinements | Unknown | 2012-03-02 |
| | |||
* | Dafny: make sure assume->assert transformation gives rise to a check | Rustan Leino | 2012-02-19 |
| | |||
* | 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: improved error location for violations of function postconditions | Rustan Leino | 2012-01-18 |
| | |||
* | Dafny: allow a refinement to provide a function/method body if the ↵ | Rustan Leino | 2012-01-18 |
| | | | | function/method being refined didn't have one | ||
* | Dafny: added signature checking to refinement | Rustan Leino | 2012-01-17 |
| | |||
* | Dafny: Recheck specifications that contain refined (extended) predicates, ↵ | Rustan Leino | 2012-01-16 |
| | | | | even if they are contained inside a split expression. Superposition is thought to be sound. | ||
* | Dafny: handle refinement of nested tokens that come from SpliExpr (still ↵ | Rustan Leino | 2012-01-12 |
| | | | | need to deal with unsplit expressions, like quantifiers) | ||
* | Dafny: some bug fixes | Rustan Leino | 2012-01-10 |
| | |||
* | 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: added support for simple superposition refinements | Rustan Leino | 2012-01-09 |
| | |||
* | Dafny: changed translation to be sensitive to refinement inheritance; this ↵ | Rustan Leino | 2012-01-09 |
| | | | | feature is now functional, provided the refining module does not add or change anything | ||
* | Dafny: disallow changes of datatypes in refinements | Rustan Leino | 2012-01-09 |
| | |||
* | Dafny: finished refinement cloning transformations | Rustan Leino | 2012-01-07 |
| | |||
* | Dafny: filled in more cloning for the refinement transformations | Rustan Leino | 2012-01-06 |
| | |||
* | Dafny: fully qualify (with module names) names of types in the translation ↵ | Rustan Leino | 2012-01-05 |
| | | | | | | | into Boogie Dafny: started cloning of refined classes Dafny: added /rprint switch to print the (syntax of the) resolved Dafny program | ||
* | Dafny: beginning of the new refinement transformations | Rustan Leino | 2012-01-05 |