dafny - 关于在 Dafny 中未验证的集合的琐碎断言

Question

教程集合包含以下代码

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

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

Answer 1

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

鲁斯坦