summaryrefslogtreecommitdiff
path: root/Test/dafny3/runtest.bat
Commit message (Expand)AuthorAge
* Added a coinductive/inductive Filter example to the test suiteGravatar Rustan Leino2013-03-18
* Added several co-induction examples from a 1996 paper by Larry Paulson.Gravatar Rustan Leino2013-03-15
* Added some test cases that show exmaples that iterate over set elements.Gravatar Rustan Leino2013-02-02
* Examples from co-induction paperGravatar Rustan Leino2013-01-22
* Added some co- test cases. Fixed some bugs.Gravatar Rustan Leino2013-01-20
* allow a refinement to introduce "return" statements, at the price of re-verif...Gravatar Rustan Leino2012-10-22
* added some calculational proofs from Dijkstra's writingsGravatar Rustan Leino2012-10-21
* Test cases for co-inductive proofs, and an axiom that makes some of them poss...Gravatar Rustan Leino2012-10-19
* Fixed some goof-ups in the test script editsGravatar Rustan Leino2012-10-04
* Added Test/dafny3 and another test file for iterators (hey, you can even run ...Gravatar Rustan Leino2012-10-04