summaryrefslogtreecommitdiff
path: root/Test/dafny3
Commit message (Expand)AuthorAge
* Don't inline opaque functions.Gravatar Rustan Leino2013-12-17
* Added some test cases: theorem about infinite and finite trees.Gravatar Rustan Leino2013-07-27
* Syntactic improvements in two tests.Gravatar Rustan Leino2013-07-16
* Added some test cases having to do with finite/infinite treesGravatar Rustan Leino2013-07-10
* Fixed soundness bug with co-recursive calls: co-recursive calls may now no l...Gravatar Rustan Leino2013-06-29
* Updated two test files.Gravatar Rustan Leino2013-03-22
* Finished support for ==# in calc, changed Paulson example to use it.Gravatar Nadia Polikarpova2013-03-20
* 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
* Renamed "parallel" statement to "forall" statement, and made the parentheses ...Gravatar Rustan Leino2013-03-06
* Changed calc syntax (custom operators are now written before the hint)Gravatar Nadia Polikarpova2013-02-08
* 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
* More automatic co-induction for comethodsGravatar Rustan Leino2013-01-20
* Added some co- test cases. Fixed some bugs.Gravatar Rustan Leino2013-01-20
* Removed the syntactic form copredicate #-form with the implicit argument.Gravatar Rustan Leino2013-01-16
* renamed "abstract module" to "module facade"Gravatar Rustan Leino2012-10-22
* 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
* Support default (which, here, means nameless) class-instance constructorsGravatar Rustan Leino2012-10-05
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 07:10:16 +0000