Dafny递归函数验证步骤疑问及相关技术咨询

function More(x: int): int
    decreases x
{
    if x <= 0 then 1 else More(x-2) + 3
}


method Example(a: int)
    // requires a == 2 // Always Verifies

    requires a > 1 && a < 3 //Fails when using var b
{
    // assert More(a) > a;  //This snippet always verifies

    var b := More(a);  // This snippet will fail when
    assert b > a;      // using the second require statement 
}

疑问解答 #

1. 预条件a==2与a>1&&a<3的验证差异 #

在整数域中，a>1&&a<3确实等价于a==2，但Dafny的验证器不会自动将范围约束简化为具体值。当使用a==2时，验证器会直接代入More(2)展开计算：More(2)=More(0)+3=1+3=4，显然4>2，赋值给b后断言自然成立。

而使用范围约束时，验证器需要对任意满足1<a<3的整数a（即a=2）证明More(a)>a，但赋值操作var b := More(a)会引入新的变量绑定，此时验证器需要泛化推理More(a)的性质，而非直接代入具体值。直接写assert More(a)>a时，验证器会直接对More(a)做展开推理，而变量赋值后需要更明确的归纳或引理支持，导致验证失败。

2. a==66通过、a==67失败的原因 #

这不是Dafny证明能力的本质限制，而是因为More函数的递归逻辑分奇偶分支：

• 当a为偶数（如66）：More(a)会递归a/2次，每次加3，最终结果为1 + 3*(a/2)，计算得1+3*33=100>66，验证器能轻松展开递归完成证明。
• 当a为奇数（如67）：More(a)会递归到x=-1（因为67-2*34=67-68=-1），结果为1 + 3*34=103>67，但验证器默认的递归展开深度或归纳搜索没有覆盖奇数分支的泛化性质。此时需要手动添加归纳引理来证明More(x)>x对所有整数x成立，而非依赖验证器自动推导。

3. 查看反例生成步骤的命令/选项 #

Dafny提供以下选项辅助分析反例：

• 使用dafny /printModel命令：会打印SMT求解器生成的模型细节，帮助识别虚假反例的来源。
• 使用dafny /proverLog:log.txt：将求解器的交互日志输出到文件，其中包含反例生成的相关过程。
• 在VSCode的Dafny插件中，开启“Show Counterexample Details”功能，可查看更结构化的反例信息。

4. 查看证明步骤的命令/选项 #

要查看Dafny的证明过程，可使用：

• dafny /proverLog:proof_log.txt：输出SMT求解器与Dafny验证器的交互日志，包含所有发送给求解器的查询和推理步骤。
• dafny /trace：跟踪验证器的内部处理流程，包括递归展开、引理应用等步骤。
• 在VSCode插件中，右键点击验证失败的断言，选择“Show Proof Attempt”，可查看可视化的证明尝试过程。

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