diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-02 14:17:15 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-02 14:17:15 -0700 |
| commit | cb24e4e69da6283835cc5f42c7b0f50dc604568d (patch) | |
| tree | 4646c1a614bfbf8a4f643fd9d651073c4a95e043 /Test/dafny0/Iterators.dfy | |
| parent | 42c116169feb1019824d43be376acded2b491a0c (diff) | |
Dafny: incomplete snapshot of verification of iterators
Diffstat (limited to 'Test/dafny0/Iterators.dfy')
| -rw-r--r-- | Test/dafny0/Iterators.dfy | 117 |
1 files changed, 115 insertions, 2 deletions
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index 76a30330..680c2812 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -11,20 +11,133 @@ iterator MyIntIter() yields (x: int, y: int) yield;
}
+iterator Naturals(u: int) yields (n: nat)
+ requires u < 25; // just to have some precondition
+ ensures false; // never ends
+{
+ n := 0;
+ while (true)
+ {
+ yield n;
+ n := n + 1;
+ }
+}
+
method Main() {
var m := new MyIter.MyIter(12);
+ assert m.ys == m.xs == [];
var a := m.x;
- // assert !a; // error: type mismatch
if (a <= 13) {
print "-- ", m.x, " --\n";
}
+ var mer := m.MoveNext();
+ if (mer) {
+ mer := m.MoveNext();
+ mer := m.MoveNext(); // error
+ }
+
var n := new MyIntIter.MyIntIter();
var patience := 10;
- while (patience != 0) {
+ while (patience != 0)
+ invariant n.Valid() && fresh(n._new);
+ {
var more := n.MoveNext();
if (!more) { break; }
print n.x, ", ", n.y, "\n";
patience := patience - 1;
}
+
+ var o := new Naturals.Naturals(18);
+ var remaining := 100;
+ while (remaining != 0)
+ invariant o.Valid() && fresh(o._new);
+ {
+ var more := o.MoveNext();
+ assert more;
+ print o.n, " ";
+ remaining := remaining - 1;
+ if (remaining % 10 == 0) { print "\n"; }
+ }
+}
+
+// -----------------------------------------------------------
+
+class Cell {
+ var data: int;
+}
+
+iterator IterA(c: Cell)
+ requires c != null;
+ modifies c;
+{
+ while (true) {
+ c.data := *;
+ yield;
+ }
+}
+
+method TestIterA()
+{
+ var c := new Cell;
+ var iter := new IterA.IterA(c);
+ var tmp := c.data;
+ var more := iter.MoveNext();
+ assert tmp == c.data; // error
+}
+
+// -----------------------------------------------------------
+
+iterator IterB(c: Cell)
+ requires c != null;
+ modifies c;
+ yield ensures c.data == old(c.data); // error: cannot prove this without a reads clause
+ ensures true;
+{
+ if (*) { yield; }
+ c.data := *;
+}
+
+method TestIterB()
+{
+ var c := new Cell;
+ var iter := new IterB.IterB(c);
+ var tmp := c.data;
+ var more := iter.MoveNext();
+ if (more) {
+ assert tmp == c.data; // no prob
+ } else {
+ assert tmp == c.data; // error: the postcondition says nothing about this
+ }
+}
+
+// -----------------------------------------------------------
+
+iterator IterC(c: Cell)
+ requires c != null;
+ modifies c;
+ reads c;
+ yield ensures c.data == old(c.data); // error: cannot prove this without a reads clause
+ ensures true;
+{
+ if (*) { yield; }
+ c.data := *;
+}
+
+method TestIterC()
+{
+ var c := new Cell;
+ var iter := new IterC.IterC(c);
+ var tmp := c.data;
+ var more := iter.MoveNext();
+ if (more) {
+ assert tmp == c.data; // no prob
+ } else {
+ assert tmp == c.data; // error: the postcondition says nothing about this
+ }
+
+ iter := new IterC.IterC(c);
+ c.data := 17;
+ more := iter.MoveNext(); // error: iter.Valid() may not hold
}
+
|