Dafny中除以10的幂次序列：断言为何失败？

你的IntValues函数逻辑本身是正确的，但Dafny的验证器无法自动推导出断言的正确性——递归函数的隐含性质需要明确的证明或规范来辅助验证。

核心问题 #

原代码中，虽然0和number/10确实会出现在生成的序列中，但Dafny不会自动归纳递归函数的所有行为，必须显式证明这些性质才能通过断言验证。

解决方案1：为函数添加后置条件 #

给IntValues添加后置条件，直接声明函数返回序列的关键性质，让Dafny利用递归的归纳性自动验证：

ghost function IntValues(n: nat) : seq<nat>
    ensures 0 in this  // 声明序列始终包含0
    ensures n != 0 ==> (n/10) in this  // 声明非0输入时，n/10必在序列中
{
    if n == 0 then [0]
    else [n] + IntValues(n/10)
}

method test_IntValues(number: nat)
{
    ghost var nvals := IntValues(number);
    assert 0 in nvals;          // 验证器现在能通过函数后置条件直接证明
    assert number/10 in nvals;  // 同理，利用第二个后置条件或第一个（当number=0时）
}

解决方案2：用辅助引理手动证明性质 #

如果不想修改函数的规范，可以在测试方法中添加辅助引理，通过归纳法证明断言的正确性：

ghost function IntValues(n: nat) : seq<nat>
{
    if n == 0 then [0]
    else [n] + IntValues(n/10)
}

method test_IntValues(number: nat)
{
    ghost var nvals := IntValues(number);
    
    // 引理1：证明IntValues(n)始终包含0
    lemma lemma_contains_zero(n: nat)
        ensures 0 in IntValues(n)
    {
        if n == 0 {
            assert IntValues(n) == [0];  // 基础情况直接验证
        } else {
            lemma_contains_zero(n/10);   // 递归调用引理处理子问题
            assert IntValues(n) == [n] + IntValues(n/10);
            assert 0 in IntValues(n/10); // 利用递归结果推导当前情况
        }
    }
    
    // 引理2：证明IntValues(n)包含n/10
    lemma lemma_contains_div10(n: nat)
        ensures (n/10) in IntValues(n)
    {
        if n == 0 {
            assert n/10 == 0;
            assert 0 in IntValues(n);
        } else {
            lemma_contains_div10(n/10);
            assert IntValues(n) == [n] + IntValues(n/10);
            // 分情况：n/10为0或非0，均能从递归结果推导
            if n/10 == 0 {
                assert 0 in IntValues(n/10);
            } else {
                assert (n/10) in IntValues(n/10);
            }
        }
    }
    
    // 调用引理后验证断言
    lemma_contains_zero(number);
    assert 0 in nvals;
    
    lemma_contains_div10(number);
    assert number/10 in nvals;
}

关键原理 #

Dafny的验证器依赖显式的逻辑规范（如后置条件）或手动证明（如引理）来确认递归函数的性质。递归函数的隐含行为不会被自动推导，必须通过归纳法或规范明确告知验证器。

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