dafny - 堆上的 Dafny 迭代器无法确保 Valid()

Question

我有一个在堆上分配迭代器并调用MoveNext()该迭代器的类。我想证明如果MoveNext()返回true，Valid()迭代器成立。

iterator Iter()
{}

class MyClass
{
    var iter : Iter;

    constructor ()
    {
        iter := new Iter();
    }
    method next() returns (more : bool)
    requires iter.Valid();
    modifies iter, iter._new, iter._modifies;
    {
        more := iter.MoveNext();
        // This assertion fails:
        assert more ==> iter.Valid();
    }
}

我查看了 的输出/rprint，并且方法MoveNext()contains ensures more ==> this.Valid()，这似乎暗示了我想要的断言。如果我将 iter 更改为在方法中本地分配next()，则 Dafny 会验证断言。

标签： dafny

Answer 1

iter._new问题是对和中的内容一无所知iter._modifies。如果this在其中一组中，则this.iter可能在调用MoveNext().

这个机构next()证实了我刚才所说的：

var i := iter;
more := iter.MoveNext();
assert i == iter;  // this assertion fails
assert more ==> iter.Valid();

因此，在假设 下more，Valid()仍然持有迭代器，但迭代器可能不再被 引用iter：

more := iter.MoveNext();
assert more ==> old(iter).Valid();  // this holds

可能您要解决此问题的方法是将前提条件添加到next()：

method next() returns (more : bool)
  requires iter.Valid()
  requires this !in iter._new + iter._modifies  // add this precondition
  modifies iter, iter._new, iter._modifies
{
  more := iter.MoveNext();
  assert more ==> iter.Valid();  // this now verifies
}

鲁斯坦