summaryrefslogtreecommitdiff
path: root/Test/dafny4/ClassRefinement.dfy
Commit message (Expand)AuthorAge
* This changeset changes the default visibility of a function/predicate body ou...Gravatar leino2015-03-09
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Fixed refinement of modify statementsGravatar Rustan Leino2014-04-04
* Also include lower set bounds (bounding a set from below) in witness guesses ...Gravatar Rustan Leino2014-04-04
* Support the transition from "modify Frame;" to "modify Frame { Body }" by ref...Gravatar Rustan Leino2014-04-04