| Commit message (Expand) | Author | Age |
* | Updated two test files. | Rustan Leino | 2013-03-22 |
* | Adjustments in the /vcsMaxKeepGoingSplits flag in the test suite | Rustan Leino | 2013-03-09 |
* | Renamed "parallel" statement to "forall" statement, and made the parentheses ... | Rustan Leino | 2013-03-06 |
* | Frame expressions are now checked to be well formed. | Rustan Leino | 2013-02-13 |
* | Fixed another specification bug in a test case. | Rustan Leino | 2013-01-23 |
* | Fixed bug in translation of method termination checks, and also fixed a (prev... | Rustan Leino | 2013-01-23 |
* | Beefed up loop invariant to prove a functional postcondition in a test case. | Rustan Leino | 2012-11-24 |
* | Beautified a test program | Rustan Leino | 2012-11-19 |
* | renamed "abstract module" to "module facade" | Rustan Leino | 2012-10-22 |
* | Fixed some goof-ups in the test script edits | Rustan Leino | 2012-10-04 |
* | Added Test/dafny3 and another test file for iterators (hey, you can even run ... | Rustan Leino | 2012-10-04 |
* | Dafny: fixed merge | Rustan Leino | 2012-10-04 |
* | Dafny: removed allocated, changed semantics of fresh | Jason Koenig | 2012-07-29 |
* | Dafny: reinstated autocontracts | Jason Koenig | 2012-07-02 |
* | Dafny: fixed up test suite (temporarily removed autocontract tests) | Jason Koenig | 2012-06-28 |
* | Dafny: fixed some test cases | Jason Koenig | 2012-06-28 |
* | Dafny: Merge | Jason Koenig | 2012-06-27 |
|\ |
|
| * | Undo bad merge. | afd | 2012-06-27 |
| * | Merge | Unknown | 2012-06-25 |
| |\ |
|
| | * | Dafny: Since it's no longer true that all types support equality at run-time ... | Unknown | 2012-06-21 |
| * | | Merge | Unknown | 2012-06-21 |
| |\| |
|
| | * | Dafny: improved refinement features; added staged version of the proof of the... | Unknown | 2012-06-19 |
| |/
|/| |
|
| * | Merged with default. | chmaria | 2012-06-18 |
| |\
| |/
|/| |
|
* | | Dafny: cleaned up test scripts a little | Unknown | 2012-06-14 |
| * | Dafny: Added tests. | chmaria | 2012-06-12 |
|/ |
|
* | Dafny: fixed regression tests | Unknown | 2012-05-29 |
* | Dafny: Added maps to regression tests. | Unknown | 2012-05-29 |
* | Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic sp... | Unknown | 2012-03-05 |
* | Dafny: fixed bug in compilation of let expressions. | Rustan Leino | 2012-01-26 |
* | Dafny: allow definitions and uses of parameter-less predicates to go without ... | Rustan Leino | 2012-01-10 |
* | Merge | Rustan Leino | 2011-11-22 |
|\ |
|
| * | Dafny: call C# compiler directly from inside Dafny, and optionally produce a ... | Rustan Leino | 2011-11-22 |
* | | Dafny: Added "type" declaration (syntax: "type X;"), which introduces an arbi... | Rustan Leino | 2011-11-21 |
|/ |
|
* | Dafny: Cleaned up proof of RevConcat in test case | Rustan Leino | 2011-11-08 |
* | Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a call to ... | Rustan Leino | 2011-11-04 |
* | Added some Dafny and Boogie test cases, including Turing's factorial program,... | Rustan Leino | 2011-11-03 |
* | Dafny induction: | Rustan Leino | 2011-10-29 |
* | Dafny: continued translation of "parallel" statements (Assign and Proof forms... | Rustan Leino | 2011-10-24 |
* | Dafny: added translation of Assign case of the parallel statement | Rustan Leino | 2011-10-22 |
* | Dafny: beautification in one test case, and fixed an Answer file | Rustan Leino | 2011-09-29 |
* | Dafny: added Flatten example to test suite | Rustan Leino | 2011-09-11 |
* | Dafny: updated Answer file from recent test additions | Rustan Leino | 2011-08-22 |
* | Dafny: updated test files (will soon update Answer files as well) | Rustan Leino | 2011-08-22 |
* | Dafny: Fixed a bug in the printer that led to a stack overflow. | wuestholz | 2011-08-11 |
* | Jennisys: started to work on synthesizing some methods. So far, only | Aleksandar Milicevic | 2011-08-10 |
* | Dafny: added reverse*reverse=id example to test suite | Rustan Leino | 2011-08-04 |
* | Dafny: re-ran parser generator to include semicolon-less body-less functions/... | Rustan Leino | 2011-07-26 |
* | Merge | Rustan Leino | 2011-07-21 |
|\ |
|
* | | Dafny: call previous lemma instead of restating it | Rustan Leino | 2011-07-21 |
| * | Fixed regression test failures due to removal of bodiless methods and functions. | Jason Koenig | 2011-07-15 |
|/ |
|