关于在 Dafny 中未验证的集合的琐碎断言答案

【问题标题】：Trivial Assertions about Sets not Verifying in Dafny关于在 Dafny 中未验证的集合的琐碎断言
【发布时间】：2017-08-22 03:28:25
【问题描述】：

教程Collections包含以下代码

method m()
{
   assert (set x | x in {0,1,2,3,4,5} && x < 3) == {0,1,2};
}

但是，目前无法在 rise4fun 提供的 Dafny 系统中进行验证：

stdin.dfy(3,11): Warning: /!\ No terms found to trigger on.
stdin.dfy(3,48): Error: assertion violation
Dafny program verifier finished with 0 verified, 1 error

这个更简单的例子

method m() { assert (set x : nat | x in {0}) == {0}; }

也不验证：

stdin.dfy(1,21): Warning: /!\ No terms found to trigger on.
stdin.dfy(1,45): Error: assertion violation
Dafny program verifier finished with 0 verified, 1 error

我认为这两个例子都应该验证；我错过了什么吗？

【问题讨论】：

标签： dafny

【解决方案1】：

这些都是真的。 Dafny 的编码中存在一个缺失条件，导致这些无法验证。我修好了它。感谢您的错误报告。

鲁斯坦

【讨论】：

亲爱的鲁斯坦，感谢您的回答。我在rise4fun 再次进行了测试，错误仍然存在，但我知道运行在那里的Dafny 系统可能需要一些时间才能更新。
我检查了源的修复。当我们下一次在那里放一个新版本时，它会去rise4fun。