Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge | 2012-09-10 | |
|\ | |||
* | | Dafny: allow 'decreases *' (that is, non-terminating recursion) on ↵ | 2012-09-09 | |
| | | | | | | | | tail-recursive methods | ||
* | | Dafny: Added detection and support for tail recursive calls (and an ↵ | 2012-09-07 | |
| | | | | | | | | optional "tailrecursion" attribute). Also, let the cloner also clone attributes. | ||
* | | Dafny: for refinements, don't consider a newly provided predicate body to be ↵ | 2012-08-30 | |
| | | | | | | | | an extension--clients don't need to be reverified if the body is new, only an extensions to a previous definition need to be | ||
| * | Dafny: allow more corecursive calls for copredicates | 2012-08-30 | |
|/ | |||
* | Dafny: fixed contract bug in resolver | 2012-08-27 | |
| | |||
* | DafnyExtension: fixed more missing cases for hover texts | 2012-08-15 | |
| | |||
* | Dafny: two bug fixes (resolution crashing on bad input, DafnyExtension ↵ | 2012-08-14 | |
| | | | | crashing after certain deletes) | ||
* | Dafny: internal renaming | 2012-08-10 | |
| | |||
* | Dafny: added heuristics for finding witnesses in assign-such-that checking | 2012-08-10 | |
| | |||
* | Dafny: corrected comment | 2012-08-03 | |
| | |||
* | 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). | ||
* | Dafny: added structural refinement check | 2012-07-29 | |
| | |||
* | Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ↵ | 2012-07-17 | |
| | | | | parallel statements. | ||
* | Dafny: compilation of abstract modules, including local definitions (as in ↵ | 2012-07-17 | |
| | | | | | | | module A as B = C) * * * Dafny: compilation of abstract modules, including local definitions (as in module A as B = C) | ||
* | Dafny: check that resolution successfully resolved all types, where appropriate. | 2012-07-12 | |
| | |||
* | Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to ↵ | 2012-07-10 | |
| | | | | parallel syntax, other minor fixes | ||
* | Merge | 2012-07-09 | |
|\ | |||
* | | Dafny: More work on the coinduction principle | 2012-07-09 | |
| | | |||
| * | Dafny: added verification that replaced expressions are the same as the original | 2012-07-09 | |
| | | |||
| * | Dafny: added named expressions and replacement | 2012-07-09 | |
| | | |||
| * | Dafny: types can now be qualified with full module paths | 2012-07-06 | |
| | | |||
| * | Dafny: datatype constructors can be accessed across module boundaries. | 2012-07-06 | |
| | | |||
| * | Dafny: fixed a crash in datatype argument resolution | 2012-07-05 | |
| | | |||
| * | Dafny: Fixed bug in autocontracts where the post resolver was run even if ↵ | 2012-07-05 | |
| | | | | | | | | there were resolution errors. | ||
| * | Dafny: disallow importing ghost modules into physical ones. | 2012-07-05 | |
| | | |||
* | | Merge | 2012-07-04 | |
|\| | |||
| * | Dafny: added static members of _default to the module level scope, at low ↵ | 2012-07-03 | |
| | | | | | | | | priority. | ||
| * | Dafny: added support for nested abstract modules, fixed some translation issues | 2012-07-03 | |
| | | |||
* | | Merge | 2012-07-03 | |
|\| | |||
* | | Dafny: added copredicates | 2012-07-03 | |
| | | |||
| * | Dafny: reinstated autocontracts | 2012-07-02 | |
|/ | |||
* | Dafny: Merge | 2012-06-27 | |
|\ | |||
* | | Dafny: fixed bug in which _module scope declarations were not verified. | 2012-06-27 | |
| | | |||
* | | Dafny: Fixed module bugs | 2012-06-27 | |
| | | |||
* | | Dafny: Implemented abstract modules | 2012-06-26 | |
| | | |||
| * | Dafny: now, equality-support determination and checking feels ripe; so, ↵ | 2012-06-22 | |
| | | | | | | | | | | | | codatatypes would then be sound Dafny: added special case to allow equality comparison against parameter-less datatype values | ||
| * | Dafny: mark code for equality-support determination tentative | 2012-06-22 | |
| | | |||
| * | Dafny: equality-support test cases. This is just a snapshot--some things ↵ | 2012-06-22 | |
| | | | | | | | | still to be fixed up. | ||
| * | Dafny: added contracts to IRewriter methods | 2012-06-22 | |
| | | |||
| * | Dafny: deal with equality-support issues in refinements | 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 ↵ | 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: Added nested modules | 2012-06-19 | |
|/ | |||
* | Dafny: in compiler, respect C#'s different scoping rules and lack of support ↵ | 2012-06-14 | |
| | | | | for special characters in identifiers | ||
* | Merge | 2012-06-13 | |
|\ | |||
* | | Dafny: allow parallel assignments to assign to the same LHS if the RHS match. | 2012-06-13 | |
| | | |||
| * | Merge | 2012-06-13 | |
| |\ | |/ |/| | |||
| * | 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: liberalized equality to work when the types could possibly be the same | 2012-06-13 | |
|/ | | | | (i.e. a != b is allowed when a: array<int> and b: array<T>) |