问Dafny无法验证while循环中的多个迭代器
EN

Stack Overflow用户

提问于 2019-08-07 03:14:04

回答 1查看 162关注 0票数 1

我想要有一个分配两个迭代器的函数，然后进入一个循环，只要MoveNext()返回true，它就会重复调用迭代器上的MoveNext()。然而，在迭代器上调用MoveNext()会违反(或阻止Dafny验证)另一个迭代器所需的不变量：

iterator Iter1()
{ yield; }

iterator Iter2()
{ yield; }

method main()
    decreases *
{
    var iter1 := new Iter1();
    var iter2 := new Iter2();
    var iter1More := true;
    var iter2More := true;

    while (iter1More || iter2More)
        invariant iter1More ==> iter1.Valid() && fresh(iter1._new)
        // The following invariant is not verified
        invariant iter2More ==> iter2.Valid() && fresh(iter2._new)
        decreases *
    {
        if (iter1More) {
            iter1More := iter1.MoveNext();
        }
    }
}

即使Iter1有一个空的modifies子句，Dafny也无法验证iter2More ==> iter2.Valid() && fresh(iter2._new)。有没有需要添加的循环不变量？

dafny

回答 1

Stack Overflow用户

回答已采纳

发布于 2019-08-07 09:19:35

好的，这个很有趣:)

下面是验证它所需的附加不变量

invariant {iter1} + iter1._new !! {iter2} + iter2._new

这个不变量也足以证明调用两个迭代器的更复杂的循环，如下所示：

    if (iterMore1) {
        iterMore1 := iter1.MoveNext();
    }
    if (iterMore2) {
        iterMore2 := iter2.MoveNext();
    }

我弄明白这一点的方法是，Dafny抱怨在调用iter1.MoveNext()之后，iter2.Valid()可能无法保持。任何时候，在调用前为真的谓词在调用后可能不为真，您知道问题是Dafny无法证明函数的reads子句与方法的modifies子句不重叠。不幸的是，迭代器的Valid()谓词的reads子句和迭代器的MoveNext()方法的modifies子句都没有文档。我深入研究了Dafny的Boogie输出，并能够对它们进行逆向工程，如下所示

predicate Valid()
  reads this, this._reads, this._new

method MoveNext()
  modifies this, this._modifies, old(this._new)

我还可以看到Dafny可以显示Iter1和Iter2都有空的_reads和_modifies集。因此，实际上只是引用本身，以及它们的_new集。这解释了不变量。

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/57382596

复制

相似问题

问Dafny无法验证while循环中的多个迭代器
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Dafny无法验证while循环中的多个迭代器EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Dafny无法验证while循环中的多个迭代器
EN