diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-03 13:31:25 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-03 13:31:25 -0700 |
| commit | 7f2783976dbdfe1392e40cf749922372f32e7ed7 (patch) | |
| tree | 0b867f4b6c284aa3bfc750fcc9e8c7d78a591732 /Test/dafny0/Iterators.dfy | |
| parent | 06c6bfd2134bd9412b909d77887673b47a88b72b (diff) | |
Dafny: more part of verifying iterators
Diffstat (limited to 'Test/dafny0/Iterators.dfy')
| -rw-r--r-- | Test/dafny0/Iterators.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index 3f06e445..36ba94cb 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -121,7 +121,7 @@ iterator IterC(c: Cell) yield ensures c.data == old(c.data);
ensures true;
{
- if (*) { yield; }
+ if (*) { yield; } // this time, all is fine, because the iterator has an appropriate reads clause
if (*) { yield; } // this time, all is fine, because the iterator has an appropriate reads clause
c.data := *;
}
|