令人惊讶的达夫妮未能验证集合理解的有界性 [英] Surprising Dafny failure to verify boundedness of set comprehension

问题描述

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

Dafny has no problem with this definition of a set intersection function.

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

但是当谈到工会时，Dafny抱怨说：一套理解必须产生一个有限集，但达夫尼的启发法无法弄清楚如何为 x产生一个有界值。

But when it comes to union, Dafny complains, "a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'". A and B are finite, and so, clearly the union is, too.

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

这对初学者看似不符的行为解释了什么？

What explains this, to-a-beginner seemingly discrepant, behavior?

推荐答案

这确实令人惊讶！

首先，让我注意到在实践中，Dafny内置了交集和并集运算符，它知道保留有限性。因此，您无需使用集合理解来表达这些想法。相反，您可以只说 A * B 和 A + B 。

First, let me note that in practice, Dafny has built-in operators for intersection and union that it knows preserve finiteness. So you don't need to use set comprehensions to express these ideas. Instead you could just say A * B and A + B respectively.

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

However, my guess is that you're running into a more complicated example where you're using a set comprehension with a disjunction and are confused about why Dafny can't prove it finite.

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

Dafny uses syntactic heuristics to determine whether a set comprehension is finite. Unfortunately, these heuristics are not well documented anywhere. For purposes of this question, the key point is that the heuristics either depend on the type of the comprehension's bound variables, or look for a conjunct that constrains elements to be bounded in some other way. For example, Dafny can prove

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

有限，以及

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

在两种情况下，相关边界都必须是合取。达夫尼（Dafny）并没有句法试探法来证明析取的界限，尽管可以想象加一。这就是Dafny无法证明您的 union 函数有限的原因。

In both cases, it is essential that the relevant bounds be conjuncts. Dafny has no syntactic heuristic for proving a bound for disjunctions, although one could imagine adding one. That is why Dafny cannot prove your union function finite.

此外，另一种解决方法是使用潜在的无限集（在Dafny中写为 iset ）。如果您不需要使用集合的基数，则可能会更好。

As an aside, another work around would be to use potentially infinite sets (written iset in Dafny). If you don't need use the cardinality of the sets, then these might work better.

这篇关于令人惊讶的达夫妮未能验证集合理解的有界性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！