Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Also updated test15 | 2012-08-14 | |
| | |||
* | Update test suite for commit 8a59fbb7ee34. | 2012-08-14 | |
| | |||
* | Dafny: added heuristics for finding witnesses in assign-such-that checking | 2012-08-10 | |
| | |||
* | Dafny: added MonotonicHeapstate refinement example | 2012-08-09 | |
| | |||
* | Dafny: fixed bug in reverifying allowing old locals to be modified. | 2012-08-01 | |
| | |||
* | Dafny: support opening modules into the local scope | 2012-07-30 | |
| | |||
* | Dafny: updated test suite to new syntax | 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: 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: fixed bug in which old locals were not properly forbidden from being ↵ | 2012-07-12 | |
| | | | | modified during refinement | ||
* | Merge | 2012-07-12 | |
|\ | |||
| * | Dafny: restored soundness for refinement by disallowing certain updates and ↵ | 2012-07-11 | |
| | | | | | | | | method calls | ||
| * | Dafny: fixed translation bug in maps with objects in the domain, added test case | 2012-07-11 | |
| | | |||
* | | Dafny: added a copredicate test case | 2012-07-11 | |
|/ | |||
* | Merge | 2012-07-10 | |
|\ | |||
| * | Merge | 2012-07-09 | |
| |\ | |||
| * | | Dafny: More work on the coinduction principle | 2012-07-09 | |
| | | | |||
| | * | Merge | 2012-07-09 | |
| | |\ | |||
| | * | | Dafny: fixed test case | 2012-07-09 | |
| | | | | |||
| | | * | GPUVerify: add beginnings of a test suite | 2012-07-04 | |
| | |/ | |||
| | * | Dafny: types can now be qualified with full module paths | 2012-07-06 | |
| |/ |/| | |||
| * | Merge | 2012-07-03 | |
| |\ | |/ |/| | |||
| * | Dafny: added copredicates | 2012-07-03 | |
| | | |||
* | | Dafny: reinstated autocontracts | 2012-07-02 | |
|/ | |||
* | Boogie: updated test15/Answer (which showed as a permutation of the previous ↵ | 2012-06-29 | |
| | | | | Answer) | ||
* | Dafny: fixed up test suite (temporarily removed autocontract tests) | 2012-06-28 | |
| | |||
* | Dafny: fixed some test cases | 2012-06-28 | |
| | |||
* | Dafny: Merge | 2012-06-27 | |
|\ | |||
| * | Undo bad merge. | 2012-06-27 | |
| | | |||
| * | Merge | 2012-06-25 | |
| |\ | |||
| | * | 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: 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. | ||
| * | | Merge | 2012-06-21 | |
| |\| | |||
| | * | Dafny: improved refinement features; added staged version of the proof of ↵ | 2012-06-19 | |
| |/ |/| | | | | | the Schorr-Waite algorithm (the staging features, as well as the newly added comments, make the verification much more digestible) | ||
| * | Merged with default. | 2012-06-18 | |
| |\ | |/ |/| | |||
| * | Dafny: Added CC translation of postconditions. | 2012-06-18 | |
| | | |||
* | | Dafny: in compiler, respect C#'s different scoping rules and lack of support ↵ | 2012-06-14 | |
| | | | | | | | | for special characters in identifiers | ||
* | | Merge | 2012-06-14 | |
|\ \ | |||
* | | | Dafny: fixed a couple of compiler bugs | 2012-06-14 | |
| | | | |||
* | | | Dafny: cleaned up test scripts a little | 2012-06-14 | |
| | | | |||
| * | | 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>) | ||
* | | | Dafny: added another version of the majority finding algorithm to the test suite | 2012-06-12 | |
|/ / |