Dafny 意外断言违规答案

【问题标题】：Dafny unexpected assertion violationDafny 意外断言违规
【发布时间】：2018-11-23 23:26:20
【问题描述】：

为什么 Dafny 无法证明这一点？

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;

}

【问题讨论】：

即使这样：assert v in (f[x:=v]).Values;.

标签： dafny

【解决方案1】：

如果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 无法证明这一点。你可以通过说来说服 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。您可能也有兴趣阅读axiomatic definition 中的.Values 原语操作。

【讨论】：

Ups，对，我的错误断言是一个很好的例子，说明在看似简单的属性中不小心。谢谢。我想知道是否有可能提供一个类似 .Values 的属性，该属性提供一个多集而不是一组值，以在我的错误断言中启用这种推理。当然也可以是用户自定义的。