令人惊讶的达夫尼失败,验证了集合理解的有界性[英] Surprising Dafny failure to verify boundedness of set comprehension

本文是小编为大家收集整理的关于令人惊讶的达夫尼失败,验证了集合理解的有界性的处理方法,想解了令人惊讶的达夫尼失败,验证了集合理解的有界性的问题怎么解决?令人惊讶的达夫尼失败,验证了集合理解的有界性问题的解决办法?那么可以参考本文帮助大家快速定位并解决问题。

问题描述

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
}

什么解释了这个,对于初学者来说,看似不一致的行为?

推荐答案

这确实令人惊讶!

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

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

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

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

有限的,以及

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

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

顺便说一句,另一种解决方法是使用潜在的无限集合(用 Dafny 编写的 iset).如果您不需要使用集合的基数,那么这些可能会更好.

本文地址:https://www.itbaoku.cn/post/1793856.html