时间戳

首页 > 解决方案 > Dafny 迭代器：违反了前提条件和修改子句

dafny - Dafny 迭代器：违反了前提条件和修改子句

问题描述

在不执行任何操作的迭代器上调用 MoveNext() 时，Dafny 显示多个错误：

iterator Iter()
{}

method main()
    decreases *
{
    var iter := new Iter();
    while (true)
        decreases *
    {
        var more := iter.MoveNext();
        if (!more) { break; }
    }
}

错误出现在对 iter.MoveNext() 的调用中：

call may violate context's modifies clause

A precondition for this call might not hold.

main 或 Iter 没有修改子句，Iter 没有前置条件。为什么这个程序不正确？

标签： dafny

解决方案

您在循环中需要以下不变量

invariant iter.Valid() && fresh(iter._new)

然后你的程序验证。像往常一样，您的程序没有任何问题（动态地），但是由于缺少注释，您在验证时可能会出现误报。

据我所知，使用迭代器时总是需要这个不变量。

（一点点）有关迭代器的更多信息可以在第 16 章的Dafny 参考中找到。（至少，有足够的信息让我记住这个问题的答案。）

推荐阅读