| Commit message (Expand) | Author | Age |
* | Merge | Rustan Leino | 2012-09-10 |
|\ |
|
* | | Dafny: allow 'decreases *' (that is, non-terminating recursion) on tail-recur... | Rustan Leino | 2012-09-09 |
* | | Dafny: Added detection and support for tail recursive calls (and an optional... | Unknown | 2012-09-07 |
* | | Dafny: for refinements, don't consider a newly provided predicate body to be ... | Unknown | 2012-08-30 |
| * | Dafny: allow more corecursive calls for copredicates | Rustan Leino | 2012-08-30 |
|/ |
|
* | Dafny: fixed contract bug in resolver | Rustan Leino | 2012-08-27 |
* | DafnyExtension: fixed more missing cases for hover texts | Unknown | 2012-08-15 |
* | Dafny: two bug fixes (resolution crashing on bad input, DafnyExtension crashi... | Unknown | 2012-08-14 |
* | Dafny: internal renaming | Unknown | 2012-08-10 |
* | Dafny: added heuristics for finding witnesses in assign-such-that checking | Unknown | 2012-08-10 |
* | Dafny: corrected comment | Jason Koenig | 2012-08-03 |
* | 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 |
* | Dafny: added structural refinement check | Jason Koenig | 2012-07-29 |
* | Dafny: allowed strictly finite datatypes in comprehensions, quantifiers, and ... | Jason Koenig | 2012-07-17 |
* | Dafny: compilation of abstract modules, including local definitions (as in mo... | Jason Koenig | 2012-07-17 |
* | Dafny: check that resolution successfully resolved all types, where appropriate. | Jason Koenig | 2012-07-12 |
* | Dafny: fixed ghost checking for labeled (i.e. named) expressions, changed to ... | Jason Koenig | 2012-07-10 |
* | Merge | Rustan Leino | 2012-07-09 |
|\ |
|
* | | Dafny: More work on the coinduction principle | Rustan Leino | 2012-07-09 |
| * | Dafny: added verification that replaced expressions are the same as the original | Jason Koenig | 2012-07-09 |
| * | Dafny: added named expressions and replacement | Jason Koenig | 2012-07-09 |
| * | Dafny: types can now be qualified with full module paths | Jason Koenig | 2012-07-06 |
| * | Dafny: datatype constructors can be accessed across module boundaries. | Jason Koenig | 2012-07-06 |
| * | Dafny: fixed a crash in datatype argument resolution | Jason Koenig | 2012-07-05 |
| * | Dafny: Fixed bug in autocontracts where the post resolver was run even if the... | Jason Koenig | 2012-07-05 |
| * | Dafny: disallow importing ghost modules into physical ones. | Jason Koenig | 2012-07-05 |
* | | Merge | Rustan Leino | 2012-07-04 |
|\| |
|
| * | Dafny: added static members of _default to the module level scope, at low pri... | Jason Koenig | 2012-07-03 |
| * | Dafny: added support for nested abstract modules, fixed some translation issues | Jason Koenig | 2012-07-03 |
* | | Merge | Rustan Leino | 2012-07-03 |
|\| |
|
* | | Dafny: added copredicates | Rustan Leino | 2012-07-03 |
| * | Dafny: reinstated autocontracts | Jason Koenig | 2012-07-02 |
|/ |
|
* | Dafny: Merge | Jason Koenig | 2012-06-27 |
|\ |
|
* | | Dafny: fixed bug in which _module scope declarations were not verified. | Jason Koenig | 2012-06-27 |
* | | Dafny: Fixed module bugs | Jason Koenig | 2012-06-27 |
* | | Dafny: Implemented abstract modules | Jason Koenig | 2012-06-26 |
| * | Dafny: now, equality-support determination and checking feels ripe; so, codat... | Rustan Leino | 2012-06-22 |
| * | Dafny: mark code for equality-support determination tentative | Unknown | 2012-06-22 |
| * | Dafny: equality-support test cases. This is just a snapshot--some things sti... | Unknown | 2012-06-22 |
| * | Dafny: added contracts to IRewriter methods | Unknown | 2012-06-22 |
| * | Dafny: deal with equality-support issues in refinements | Unknown | 2012-06-22 |
| * | Dafny: Since it's no longer true that all types support equality at run-time ... | Unknown | 2012-06-21 |
* | | Dafny: Added nested modules | Jason Koenig | 2012-06-19 |
|/ |
|
* | Dafny: in compiler, respect C#'s different scoping rules and lack of support ... | Unknown | 2012-06-14 |
* | Merge | Jason Koenig | 2012-06-13 |
|\ |
|
* | | Dafny: allow parallel assignments to assign to the same LHS if the RHS match. | Jason Koenig | 2012-06-13 |
| * | Merge | Unknown | 2012-06-13 |
| |\
| |/
|/| |
|
| * | Dafny: Changed the semantics of the assign-such-that statement "x :| P;" to c... | Unknown | 2012-06-13 |
* | | Dafny: liberalized equality to work when the types could possibly be the same | Jason Koenig | 2012-06-13 |
|/ |
|