summaryrefslogtreecommitdiff
path: root/Test/dafny1/Answer
Commit message (Expand)AuthorAge
* Dafny: reinstated autocontractsGravatar Jason Koenig2012-07-02
* Dafny: fixed up test suite (temporarily removed autocontract tests)Gravatar Jason Koenig2012-06-28
* Dafny: improved refinement features; added staged version of the proof of the...Gravatar Unknown2012-06-19
* Dafny: cleaned up test scripts a littleGravatar Unknown2012-06-14
* Dafny: fixed regression testsGravatar Unknown2012-05-29
* Dafny: added experimental feature {:autocontracts} to de-clutter idiomatic sp...Gravatar Unknown2012-03-05
* Added some Dafny and Boogie test cases, including Turing's factorial program,...Gravatar Rustan Leino2011-11-03
* Dafny induction:Gravatar Rustan Leino2011-10-29
* Dafny: added Flatten example to test suiteGravatar Rustan Leino2011-09-11
* Dafny: updated Answer file from recent test additionsGravatar Rustan Leino2011-08-22
* Dafny: added reverse*reverse=id example to test suiteGravatar Rustan Leino2011-08-04
* Dafny: re-ran parser generator to include semicolon-less body-less functions/...Gravatar Rustan Leino2011-07-26
* Fixed regression test failures due to removal of bodiless methods and functions.Gravatar Jason Koenig2011-07-15
* Dafny: fixed bug in induction-tactic heuristic (should never pick values whos...Gravatar Rustan Leino2011-05-26
* Dafny: added some test cases that use natGravatar Rustan Leino2011-05-16
* Dafny:Gravatar Rustan Leino2011-05-11
* Dafny: Alternative (and candidate replacement) syntax for declaring datatypesGravatar Rustan Leino2011-04-20
* Dafny: fixed bug in induction over integersGravatar Unknown2011-04-04
* Dafny:Gravatar rustanleino2011-03-30
* Dafny: added "choose" operator on setsGravatar rustanleino2011-03-26
* Dafny: compile quantifiersGravatar rustanleino2011-03-26
* Dafny:Gravatar rustanleino2011-03-06
* Dafny:Gravatar rustanleino2011-03-04
* Dafny: added test harness to Test/dafny1/ExtensibleArray.dfyGravatar rustanleino2011-02-16
* Dafny: added ExtensibleArray program as a testGravatar rustanleino2011-02-16
* Dafny: implemented a more precise scheme for allowing use of a function's rep...Gravatar rustanleino2011-02-03
* Dafny: added ensures clauses to functionsGravatar rustanleino2011-02-02
* Dafny: Added Test/dafny1/PriorityQueue.dfyGravatar rustanleino2010-12-10
* Test/dafny1/KatzManna.dfy: Changed mocked up matrix class to use Dafny's bui...Gravatar rustanleino2010-10-27
* Boogie:Gravatar rustanleino2010-10-26
* Dafny: Compilation of multi-dimensional arraysGravatar rustanleino2010-09-21
* Dafny:Gravatar rustanleino2010-09-17
* Dafny: Axiom about inverting a set union operation, similar to the recent on...Gravatar rustanleino2010-07-09
* Dafny:Gravatar rustanleino2010-06-24
* Boogie:Gravatar rustanleino2010-06-08