使用自动合同的类的上下文修改子句冲突
使用自动合同的类的上下文修改子句冲突
提问于 2022-10-18 02:14:35
我在Dafny中有一个带有autocontracts的简单类，它创建了自己的一个新实例。
但是达夫尼说，当我在foo.Add()方法中调用Bar时，“调用可能违反上下文的修改子句”
我不知道为什么会有这个错误，因为这个类没有任何属性
我是不是遗漏了什么？
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的Dafny版本
the installed Dafny version is the latest known: 3.9.0.41003 = 3.9.0回答 1
Stack Overflow用户
回答已采纳
发布于 2022-10-18 03:34:28
我想你可能过于简化了你的例子，因为我不确定我是否理解你的问题。
我想你要找的答案是你应该删除这一行
modifies fo从循环中添加行
invariant fresh(fo.Repr)这修复了有关违反上下文的修改子句的错误。
您没有提到的代码中的其余错误，但这与Bar的autocontracts Post条件有关，该条件是
this.Valid() && fresh(this.Repr - old(this.Repr))这是双重混淆的，因为Foo类没有字段，而且Bar方法从来没有提到this。因此，一个解决办法是使Bar成为一个static方法。
或者，如果在原始设置中需要Bar为非静态设置，则可以添加不变量。
invariant this.Valid() && fresh(this.Repr - old(this.Repr))以修复第二个错误。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/74104958
复制相关文章
相似问题
腾讯云开发者
