summaryrefslogtreecommitdiff
path: root/Test/dafny0/Corecursion.dfy
Commit message (Expand)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Added further assistance in coming up with decreases clauses in SCCs with co-...Gravatar Rustan Leino2014-02-24
* Refactored code for dealing with SCCs in the call graph.Gravatar Rustan Leino2014-02-24
* Introduced keywords "lemma" (like a "ghost method", but not allowed to have a...Gravatar Rustan Leino2013-08-02
* Co-recursion, now sounder than ever!Gravatar Rustan Leino2013-07-30
* Fixed soundness bug with co-recursive calls: co-recursive calls may now no l...Gravatar Rustan Leino2013-06-29
* Fixed unsoundness (and also allowed other, sound cases) in the admissability ...Gravatar Rustan Leino2013-06-28
* changed default decreases clause for functions with a reads clause: use the r...Gravatar Rustan Leino2012-10-04
* Dafny: more correct checking of co-inductive productivityGravatar Unknown2012-05-18
* Dafny: added support for co-recursive callsGravatar Rustan Leino2012-05-01