令人惊讶的是，达夫尼未能验证集合理解的有界性

Dafny 对于集合交集函数的定义没有任何问题。

function method intersection(A: set<int>, B: set<int>): (r: set<int>)
{
    set x | x in A && x in B
}

但当谈到并集时，达夫尼抱怨道，“集合理解必须产生有限集，但达夫尼的启发式方法无法弄清楚如何产生‘x’的有界值集”。 A 和 B 是有限的，因此，显然并集也是有限的。

function method union(A: set<int>, B: set<int>): (r: set<int>)
{
    set x | x in A || x in B
}

对于初学者来说，如何解释这种看似不一致的行为？

这确实可能令人惊讶！

首先，让我注意到，在实践中，Dafny 有内置的交集和并集运算符，它知道这些运算符保留了有限性。因此，您不需要使用集合推导式来表达这些想法。相反你可以说A * B and A + B分别。

然而，我的猜测是，您遇到了一个更复杂的示例，其中您使用了带有析取的集合理解，并且对为什么 Dafny 无法证明它是有限的感到困惑。

Dafny 使用句法启发式来确定集合推导式是否是有限的。不幸的是，这些启发式方法在任何地方都没有得到很好的记录。就这个问题而言，关键点是启发式要么依赖于推导式的绑定变量的类型，要么寻找以其他方式约束元素的合取。例如，达夫尼可以证明

set x: int | 0 <= x < 10 && ...

有限的，以及

set x:A | x in S && ...

在这两种情况下，相关界限必须是连词。达夫尼没有语法启发法来证明析取的界限，尽管人们可以想象添加一个。这就是为什么达夫尼无法证明你的union函数有限。

顺便说一句，另一种解决方法是使用潜在的无限集（写成iset在达夫尼）。如果您不需要使用集合的基数，那么这些可能会更好。