summaryrefslogtreecommitdiff
path: root/Test/dafny0/Refinement.dfy
Commit message (Expand)AuthorAge
* This changeset changes the default visibility of a function/predicate body ou...Gravatar leino2015-03-09
* Stop pretty-print from emitting deprecated semi-colons.Gravatar qunyanm2015-03-05
* Language change: All functions and methods declared lexically outside any cla...Gravatar leino2014-12-12
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Make functions and predicates be opaque outside the defining module -- only t...Gravatar Rustan Leino2013-07-29
* Dafny: updated test suite to new syntaxGravatar Jason Koenig2012-07-30
* Dafny: fixed some test casesGravatar Jason Koenig2012-06-28
* Dafny: make sure assume->assert transformation gives rise to a checkGravatar Rustan Leino2012-02-19
* Dafny: added syntactic support for ...'s in statements, and started implement...Gravatar Unknown2012-02-18
* Dafny: allow signatures to be omitted on refining functions/methodsGravatar Unknown2012-02-16
* Dafny: improved error location for violations of function postconditionsGravatar Rustan Leino2012-01-18
* Dafny: allow a refinement to provide a function/method body if the function/m...Gravatar Rustan Leino2012-01-18
* Dafny: added signature checking to refinementGravatar Rustan Leino2012-01-17
* Dafny: allow class-member declarations at top level of any module (not just t...Gravatar Rustan Leino2012-01-10
* Dafny: added test case for refinement and predicates (and fixed a parsing bug)Gravatar Rustan Leino2012-01-10
* Dafny: added support for simple superposition refinementsGravatar Rustan Leino2012-01-09
* Dafny: added assertions in the refinement obligation necessitating that the r...Gravatar kyessenov2010-07-03
* Dafny: Support class type parameters in refinements. Added another regression...Gravatar kyessenov2010-07-02
* Dafny: added Carrol Morgan's calculator regression test.Gravatar kyessenov2010-07-02