summaryrefslogtreecommitdiff
path: root/Test/dafny1/Celebrity.dfy
Commit message (Expand)AuthorAge
* Language change: All functions and methods declared lexically outside any cla...Gravatar leino2014-12-12
* New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* The "choose" statement, hacky and specialized as it was, is now gone. Use th...Gravatar Rustan Leino2013-03-27
* Dafny: Since it's no longer true that all types support equality at run-time ...Gravatar Unknown2012-06-21
* 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: allow constructors only inside classes, removed semi-colons at end of ...Gravatar Rustan Leino2011-07-11
* Dafny: don't require parentheses in syntax of "choose" statementsGravatar Rustan Leino2011-04-05
* Dafny: added "choose" operator on setsGravatar rustanleino2011-03-26
* Dafny: improved and corrected physical/ghost distinctionGravatar rustanleino2011-03-26
* Dafny: Fix type bug in SplitExpr translation.Gravatar rustanleino2010-06-08
* Boogie:Gravatar rustanleino2010-06-08