1

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

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

但是当谈到联合时，Dafny 抱怨道，“集合推导必须产生一个有限集合，但 Dafny 的启发式算法无法弄清楚如何为 'x' 产生一组有界值”。A 和 B 是有限的，因此显然联合也是。

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

是什么解释了这种对初学者来说看似不一致的行为？

4

1 回答 1

1

这确实可能令人惊讶！

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

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

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

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

有限的，以及

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

在这两种情况下，相关边界必须是合取的。Dafny 没有语法启发式来证明析取的界限，尽管可以想象添加一个。这就是为什么 Dafny 不能证明你的union函数是有限的。

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

于 2018-03-14T17:30:08.817 回答