问Dafny意外断言冲突
EN

Stack Overflow用户

提问于 2018-06-14 16:39:16

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

为什么达夫尼不能证明这一点？

method Main() {

assert forall f:map<string,int>, x:string, v:int :: x in f.Keys  ==>  f.Values- 
{f[x]} + {v} == (f[x:=v]).Values;

}

dafny

回答 1

Stack Overflow用户

发布于 2018-06-15 01:55:08

如果f包含重复的值，则断言不为真。例如，考虑地图

var f := map[1 := 0, 2 := 0];

哪一项满足

assert f.Values == {0};

现在通过将关键字1设置为具有值7来生成更新的映射，

var f' := f[1 := 7];

然后是f'[1] == 7和f'[2] == 0，所以f'满足

assert f'.Values == {0, 7};

但是您的断言将暗示f'.Values == {0}，这是错误的。

对于你在评论中提出的第二个问题，断言是正确的，但Dafny无法证明这一点，因为触发问题。你可以说服达夫尼来证明这一点

var f' := f[x:=v];          // give updated map a name for convenience
assert f'[x] in f'.Values;  // triggers axiom about .Values
assert v in f'.Values;      // now this verifies

有关触发器的详细信息，请参阅FAQ。您可能还有兴趣阅读.Values原语操作的axiomatic definition。

票数 1

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

原文链接：

https://stackoverflow.com/questions/50853171

复制

相似问题

问Dafny意外断言冲突
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Dafny意外断言冲突EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Dafny意外断言冲突
EN