| Commit message (Expand) | Author | Age |
* | 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 |
|/ |
|
* | Dafny: allow constructors only inside classes, removed semi-colons at end of ... | Rustan Leino | 2011-07-11 |
* | Dafny: Translate general LHSs for var and := (not yet for call, no compilatio... | Rustan Leino | 2011-05-30 |
* | Merge | Rustan Leino | 2011-05-27 |
|\ |
|
| * | Dafny: permanently changed the syntax of "datatype" declarations to what prev... | Rustan Leino | 2011-05-27 |
| * | Dafny: | Rustan Leino | 2011-05-26 |
* | | Dafny: fixed bug in induction-tactic heuristic (should never pick values whos... | Rustan Leino | 2011-05-26 |
| * | Dafny: retired the "call" keyword | Rustan Leino | 2011-05-26 |
| * | Dafny: | Rustan Leino | 2011-05-21 |
|/ |
|
* | Dafny: added some test cases that use nat | Rustan Leino | 2011-05-16 |
* | Merge | Rustan Leino | 2011-05-13 |
|\ |
|
| * | Dafny: | Rustan Leino | 2011-05-11 |
* | | Dafny: fixed compilation bugs, added @-signs in front of identifiers to avoid... | Rustan Leino | 2011-05-11 |
|/ |
|
* | Dafny: Fix parsing of if-then-else expressions, and don't require parentheses... | Rustan Leino | 2011-04-21 |
* | Dafny: Alternative (and candidate replacement) syntax for declaring datatypes | Rustan Leino | 2011-04-20 |
* | Dafny: added manual proofs for 5 theorems in Rippling.dfy | Rustan Leino | 2011-04-12 |
* | Dafny: don't require parentheses in syntax of "choose" statements | Rustan Leino | 2011-04-05 |
* | branch merge | Rustan Leino | 2011-04-05 |
|\ |
|
* | | Dafny: Allow field selections and array-element selection as LHSs of assignme... | Unknown | 2011-04-05 |
| * | Dafny: fixed bug in induction over integers | Unknown | 2011-04-04 |
|/ |
|
* | Dafny: | rustanleino | 2011-03-30 |
* | Dafny: Added support for an initializing call as part of the new-allocation s... | rustanleino | 2011-03-27 |
* | Dafny: added "choose" operator on sets | rustanleino | 2011-03-26 |
* | Dafny: improved and corrected physical/ghost distinction | rustanleino | 2011-03-26 |
* | Dafny: compile quantifiers | rustanleino | 2011-03-26 |
* | Dafny: Fixed typo in P16 of Rippling benchmarks, which now makes it (true and... | rustanleino | 2011-03-07 |
* | Dafny: | rustanleino | 2011-03-06 |
* | Dafny: Added heuristic for when to turn on the induction tactic | rustanleino | 2011-03-05 |
* | Dafny: | rustanleino | 2011-03-04 |
* | Dafny: | rustanleino | 2011-02-17 |