From cb24e4e69da6283835cc5f42c7b0f50dc604568d Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 2 Oct 2012 14:17:15 -0700 Subject: Dafny: incomplete snapshot of verification of iterators --- Test/dafny0/Answer | 25 +++++--- Test/dafny0/IteratorResolution.dfy | 8 +++ Test/dafny0/Iterators.dfy | 117 ++++++++++++++++++++++++++++++++++++- 3 files changed, 141 insertions(+), 9 deletions(-) (limited to 'Test/dafny0') diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index bde6a07c..ecde4fb1 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1616,16 +1616,27 @@ TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive met 5 resolution/type errors detected in TailCalls.dfy -------------------- IteratorResolution.dfy -------------------- -IteratorResolution.dfy(56,11): Error: LHS of assignment does not denote a mutable field -IteratorResolution.dfy(57,11): Error: LHS of assignment does not denote a mutable field -IteratorResolution.dfy(61,18): Error: arguments must have the same type (got _T0 and int) -IteratorResolution.dfy(73,19): Error: RHS (of type bool) not assignable to LHS (of type int) -IteratorResolution.dfy(76,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called -5 resolution/type errors detected in IteratorResolution.dfy +IteratorResolution.dfy(59,11): Error: LHS of assignment does not denote a mutable field +IteratorResolution.dfy(60,11): Error: LHS of assignment does not denote a mutable field +IteratorResolution.dfy(64,18): Error: arguments must have the same type (got _T0 and int) +IteratorResolution.dfy(76,19): Error: RHS (of type bool) not assignable to LHS (of type int) +IteratorResolution.dfy(79,13): Error: when allocating an object of type 'GenericIteratorResult', one of its constructor methods must be called +IteratorResolution.dfy(83,15): Error: logical negation expects a boolean argument (instead got int) +IteratorResolution.dfy(17,11): Error: LHS of assignment does not denote a mutable field +IteratorResolution.dfy(18,11): Error: LHS of assignment does not denote a mutable field +IteratorResolution.dfy(19,12): Error: LHS of assignment does not denote a mutable field +9 resolution/type errors detected in IteratorResolution.dfy -------------------- Iterators.dfy -------------------- +Iterators.dfy(36,14): Error BP5002: A precondition for this call might not hold. +Iterators.dfy(1,10): Related location: This is the precondition that might not hold. +Execution trace: + (0,0): anon0 + (0,0): anon31_Then + (0,0): anon3 + (0,0): anon32_Then -Dafny program verifier finished with 8 verified, 0 errors +Dafny program verifier finished with 16 verified, 1 error -------------------- Superposition.dfy -------------------- diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy index fe9e2563..dca4cb93 100644 --- a/Test/dafny0/IteratorResolution.dfy +++ b/Test/dafny0/IteratorResolution.dfy @@ -14,6 +14,9 @@ module Mx { method IteratorUser() { var iter := new ExampleIterator.ExampleIterator(15); + iter.k := 12; // error: not allowed to assign to iterator's in-parameters + iter.x := 12; // error: not allowed to assign to iterator's yield-parameters + iter.xs := []; // error: not allowed to assign to iterator's yield-history variables var j := 0; while (j < 100) { var more := iter.MoveNext(); @@ -74,6 +77,11 @@ module Mx { } var h2 := new GenericIteratorResult; // error: constructor is not mentioned + + var h3 := new GenericIterator.GenericIterator(30); + if (h3.t == h3.u) { + assert !h3.t; // error: type mismatch + } } } 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 } + -- cgit v1.2.3