dafny - Dafny flatten 套装

Question

所以我试图从一组集合中获取所有元素，但出现错误：

“集合理解必须产生一个有限集合，但 Dafny 的启发式无法弄清楚如何为 'x' 产生一组有界值”

我认为这可能与您无法获得集合的基数有关。

感谢所有帮助。

function flatten(nested: set<set<int>>) : set<int>
    { set x | forall y :: y in nested && x in y :: x }

Answer 1

也许以下会做你想要的：

function flatten(nested: set<set<int>>) : set<int>
{
    set x, y | y in nested && x in y :: x
}

你的定义完全不同。它说的是“一组元素，使得对于所有y类型set<int>，y在nested和x在中y。” 这通常是错误的（因此无用），因为它要求它nested是一个包含所有类型集的有限集set<int>。

最后，还请注意，您可以S使用表达式获取集合的基数|S|。