summaryrefslogtreecommitdiff
path: root/Test/dafny0/Termination.dfy
Commit message (Expand)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Fixed bug in translation of method termination checks, and also fixed a (prev...Gravatar Rustan Leino2013-01-23
* Added/fixed decreases clauses that use multisets or maps.Gravatar Unknown2012-10-16
* changed default decreases clause for functions with a reads clause: use the r...Gravatar Rustan Leino2012-10-04
* Dafny: now, equality-support determination and checking feels ripe; so, codat...Gravatar Rustan Leino2012-06-22
* Fixed failing regression tests.Gravatar Jason Koenig2011-07-14
* Dafny: allow constructors only inside classes, removed semi-colons at end of ...Gravatar Rustan Leino2011-07-11
* Dafny: permanently changed the syntax of "datatype" declarations to what prev...Gravatar Rustan Leino2011-05-27
* Dafny: retired the "call" keywordGravatar Rustan Leino2011-05-26
* Dafny:Gravatar Rustan Leino2011-05-21
* Dafny: Added heuristic for when to turn on the induction tacticGravatar rustanleino2011-03-05
* Dafny:Gravatar rustanleino2011-02-17
* Dafny: every decreases clause implicitly ends with a never-ending sequence of...Gravatar rustanleino2011-02-03
* Dafny:Gravatar rustanleino2010-06-24
* Dafny:Gravatar rustanleino2010-06-19
* Dafny: Added two additional heuristics for guessing missing loop decreases c...Gravatar rustanleino2010-06-11
* Added resolution and translation of algebraic datatypes and (in function bodi...Gravatar rustanleino2009-11-20
* The Dafny call statement now automatically declares left-hand sides as local ...Gravatar rustanleino2009-11-05
* Initial set of files.Gravatar mikebarnett2009-07-15