Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Dafny: Added compiler tests. | chmaria | 2012-06-11 | |
| | | ||||
* | | Dafny: added some test programs | Rustan Leino | 2012-06-08 | |
|/ | ||||
* | Dafny: Added map comprehensions and updated display syntax | Unknown | 2012-05-31 | |
| | ||||
* | Dafny: fixed regression tests | Unknown | 2012-05-29 | |
| | ||||
* | Dafny: Added maps to regression tests. | Unknown | 2012-05-29 | |
| | ||||
* | Dafny: more correct checking of co-inductive productivity | Unknown | 2012-05-18 | |
| | ||||
* | Dafny: added support for co-recursive calls | Rustan Leino | 2012-05-01 | |
| | ||||
* | Dafny: fixed unsoundness having to do with a function depending on the ↵ | Unknown | 2012-04-27 | |
| | | | | allocation state | |||
* | Dafny: added resolution tests cases for inductive datatypes | Unknown | 2012-04-27 | |
| | ||||
* | 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: fixed lack of assign-such-that restriction in parallel statement | Unknown | 2012-03-15 | |
| | ||||
* | Dafny: added assign-such-that statements; syntax: x,y,a[i],o.f :| Expr; | Unknown | 2012-03-15 | |
| | ||||
* | Dafny: added StoreAndRetrieve refinement example | Unknown | 2012-03-15 | |
| | ||||
* | Dafny: removed a now-inferred type-parameter instantiation in a test file | Unknown | 2012-03-07 | |
| | ||||
* | 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: added experimental feature {:autocontracts} to de-clutter idiomatic ↵ | Unknown | 2012-03-05 | |
| | | | | specifications | |||
* | Merge | Unknown | 2012-03-02 | |
|\ | ||||
* | | Dafny: tests for skeletons | Unknown | 2012-03-02 | |
| | | ||||
* | | Dafny: allow more skeleton statements in refinements | Unknown | 2012-03-02 | |
| | | ||||
| * | Dafny: fixed well-formedness checking of LET expressions to allow the RHS to ↵ | Rustan Leino | 2012-02-29 | |
|/ | | | | be used | |||
* | 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: allow various forms of leaving off type arguments in declarations | Rustan Leino | 2012-02-16 | |
| | ||||
* | Dafny: fixed bug in compilation of let expressions. | Rustan Leino | 2012-01-26 | |
| | ||||
* | Dafny: Fixed a bug in the printing of let expressions. | wuestholz | 2012-01-24 | |
| | ||||
* | 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: allow parallel statements with an empty list of bound variables | Rustan Leino | 2012-01-17 | |
| | ||||
* | Dafny: parallel statements: | Rustan Leino | 2012-01-17 | |
| | | | | | | | - removed the awkward restriction that method postconditions cannot use old/fresh if there's no modifies clause and no out-parameters; instead, implemented parallel statements to handle these cases - also allow old/fresh in ensures clauses of parallel statements - allow TypeRhs and choose expressions in Call/Proof parallel statements - disallow calls to non-ghost methods in parallel statements (since those may do "print" statements and we don't want to allow those to take place in parallel; besides, the compiler wants to omit the parallel statement altogether and could not do so if there were print statements) | |||
* | 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: make full predicate definitions available only inside a module ↵ | Rustan Leino | 2012-01-11 | |
| | | | | (outside is just an implication: the predicate implies the body known so far) | |||
* | Dafny: allow class-member declarations at top level of any module (not just ↵ | Rustan Leino | 2012-01-10 | |
| | | | | the default module); these go into the (new) default class of each module | |||
* | Dafny: added test case for refinement and predicates (and fixed a parsing bug) | 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: firmed up the module system | Rustan Leino | 2012-01-05 | |
| | ||||
* | Dafny: disengaged old refinement test files | Rustan Leino | 2012-01-04 | |
| | ||||
* | Dafny: don't allow ghost expressions in print statements | Rustan Leino | 2012-01-03 | |
| | ||||
* | 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: for a datatype with just one constructor, don't check (but do assume) ↵ | Rustan Leino | 2011-12-19 | |
| | | | | that destructors are applied only to those values constructed by that one-and-only constructor | |||
* | Dafny: Made sure that error locations refer to the Dafny program, even if ↵ | wuestholz | 2011-12-15 | |
| | | | | the /print option is used. | |||
* | Dafny: Added support for attributes on various specification constructs ↵ | wuestholz | 2011-12-07 | |
| | | | | (assert, ensures, modifies, decreases, invariant). | |||
* | Dafny: implemented thresholds for the new interval domain (/infer:j) | Rustan Leino | 2011-12-12 | |
| |