summaryrefslogtreecommitdiff
path: root/Test/dafny0/Iterators.dfy
Commit message (Collapse)AuthorAge
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
|
* Set up call-graph to keep track of edges between functions and methods. (To ↵Gravatar Rustan Leino2013-08-04
| | | | be done: replace InMethodContext with a Function/Method-Height in translator.)
* Renamed "parallel" statement to "forall" statement, and made the parentheses ↵Gravatar Rustan Leino2013-03-06
| | | | around the bound variables optional.
* Support default (which, here, means nameless) class-instance constructorsGravatar Rustan Leino2012-10-05
|
* Dafny: complete implementation of iteratorsGravatar Rustan Leino2012-10-03
|
* Dafny: automatically update iterator _new field upon allocationsGravatar Rustan Leino2012-10-03
|
* Dafny: good error locations for yield statements; other iterator ↵Gravatar Rustan Leino2012-10-03
| | | | improvements / bug fixes
* Dafny: more part of verifying iteratorsGravatar Rustan Leino2012-10-03
|
* Dafny: changed iterator body to resolve to implicit fields rather than to ↵Gravatar Rustan Leino2012-10-02
| | | | the formal in- and yield-parameters
* Dafny: incomplete snapshot of verification of iteratorsGravatar Rustan Leino2012-10-02
|
* Dafny: compile iteratorsGravatar Rustan Leino2012-09-26