summaryrefslogtreecommitdiff
path: root/Test/dafny3
Commit message (Expand)AuthorAge
* renamed "abstract module" to "module facade"Gravatar Rustan Leino2012-10-22
* allow a refinement to introduce "return" statements, at the price of re-verif...Gravatar Rustan Leino2012-10-22
* added some calculational proofs from Dijkstra's writingsGravatar Rustan Leino2012-10-21
* Test cases for co-inductive proofs, and an axiom that makes some of them poss...Gravatar Rustan Leino2012-10-19
* Support default (which, here, means nameless) class-instance constructorsGravatar Rustan Leino2012-10-05
* Fixed some goof-ups in the test script editsGravatar Rustan Leino2012-10-04
* Added Test/dafny3 and another test file for iterators (hey, you can even run ...Gravatar Rustan Leino2012-10-04