Dafny验证超时原因及通用断言验证相关技术问询

问题场景 #

以下Dafny代码在验证时会出现“20秒后超时”的失败情况：

predicate DivideBy2(x: int)
{
    x % 2 == 0
}

predicate DivideBy4(x: int)
{
    x % 4 == 0
}

predicate DivideBy3(x: int)
{
    x % 3 == 0
}

method test()
    ensures DivideBy3(12)
{
    assert forall x: int | DivideBy4(x) :: DivideBy2(x);
    assert forall x: int :: DivideBy4(x) ==> DivideBy2(x);
}

移除方法体中的两个断言，或将后置条件改为方法体内的断言时，验证可通过。针对该场景提出以下问题：

1. 此处验证超时的原因是什么？
2. 方法体内的断言未限定输入范围，Dafny如何验证这类抽象逻辑？
3. 方法体内的两个断言是否存在区别？我看起来二者一致。

问题解答 #

1. 验证超时的原因 #

Dafny的验证器在处理全域量词断言+方法后置条件的组合时，会触发更复杂的验证路径。当方法存在ensures后置条件时，验证器会尝试将断言的全域属性与方法契约关联，加上整数模运算属于SMT求解器中开销较高的理论领域，两个全域断言同时存在会让求解器需要处理大量约束组合，最终超出默认时间限制导致超时。

简单来说，方法后置条件和内部全域断言形成了交叉约束，让SMT求解器的搜索空间急剧膨胀，拖慢了验证速度。

2. Dafny验证无范围限定抽象逻辑的方式 #

Dafny依赖**SMT求解器（默认是Z3）**处理这类无范围的全域断言：

• 求解器不会枚举所有整数，而是通过符号化的数学推理来证明断言的普遍性。比如利用整数模运算的性质：若x%4==0，则x是4的倍数，而4是2的倍数，因此x必然是2的倍数，以此推导DivideBy4(x)蕴含DivideBy2(x)。
• 它通过逻辑链推导、数学归纳等方法，确认断言对所有整数成立，若找不到反例且逻辑推导闭环，就判定断言有效。

3. 两个断言的区别 #

这两个断言逻辑语义完全等价，但在Dafny的验证处理流程中有细微语法层面的差异：

• 第一个断言forall x: int | DivideBy4(x) :: DivideBy2(x)是带过滤条件的全域量词写法，仅对满足DivideBy4(x)的x断言DivideBy2(x)成立。
• 第二个断言forall x: int :: DivideBy4(x) ==> DivideBy2(x)是带蕴含式的全域量词写法，对所有x断言“如果DivideBy4(x)成立则DivideBy2(x)成立”。

二者的逻辑含义没有区别，但Dafny对两种写法的语法解析和约束生成顺序略有不同，不过在这个场景中，二者共同存在才是导致超时的核心原因，单独存在时验证器都能快速完成验证。

内容的提问来源于stack exchange，提问作者ZhouTi