Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Renamed "parallel" statement to "forall" statement, and made the parentheses ↵ | Rustan Leino | 2013-03-06 |
| | | | | around the bound variables optional. | ||
* | Support default (which, here, means nameless) class-instance constructors | Rustan Leino | 2012-10-05 |
| | |||
* | Dafny: complete implementation of iterators | Rustan Leino | 2012-10-03 |
| | |||
* | Dafny: automatically update iterator _new field upon allocations | Rustan Leino | 2012-10-03 |
| | |||
* | Dafny: good error locations for yield statements; other iterator ↵ | Rustan Leino | 2012-10-03 |
| | | | | improvements / bug fixes | ||
* | Dafny: more part of verifying iterators | Rustan Leino | 2012-10-03 |
| | |||
* | Dafny: changed iterator body to resolve to implicit fields rather than to ↵ | Rustan Leino | 2012-10-02 |
| | | | | the formal in- and yield-parameters | ||
* | Dafny: incomplete snapshot of verification of iterators | Rustan Leino | 2012-10-02 |
| | |||
* | Dafny: compile iterators | Rustan Leino | 2012-09-26 |