上下文修改了具有自动契约的类的子句违规

Question

我在Dafny中有一个带有自动约束的简单类，它创建了自己的一个新实例。

但是Dafny说"；调用可能违反上下文的modifies子句"；当我在Bar方法中调用foo.Add()时

我不知道为什么我会得到这个错误，因为类没有任何属性

我是不是错过了什么？

class {:autocontracts} Foo {
predicate Valid()
constructor() { }
method Add() returns (b:bool)
method Bar() returns (fo:Foo)
ensures fresh(fo)
{
fo := new Foo();
var i := 0;
while(i < 3)
modifies fo
invariant fo.Valid()
{
var ret := fo.Add(); //call might violate context's modifies clause Verifier
i := 1 + i;
}
}
}

愚蠢版本在VSCode

the installed Dafny version is the latest known: 3.9.0.41003 = 3.9.0

Answer 1

我认为你可能过于简化了你的例子，因为我不确定我是否理解你的问题。

我认为你正在寻找的答案是，你应该删除行

modifies fo

从循环中添加线路

invariant fresh(fo.Repr)

这修复了有关违反上下文的modifies子句的错误。

代码中的剩余错误您没有提到，但它与Bar的自动打印后条件有关，即

this.Valid() && fresh(this.Repr - old(this.Repr))

由于Foo类没有字段，并且Bar方法从未提及this，因此这会使人更加困惑。因此，一个解决方案是将Bar设置为static方法。

或者，如果在您的原始设置中，您需要Bar是非静态的，那么您可以添加不变的

invariant this.Valid() && fresh(this.Repr - old(this.Repr))

到循环以修复第二个错误。