Dafny对递归调用的数量有限制吗？

问题描述

以下代码验证：

function stepMany(i : int,steps : int) : int
    requires steps >= 0;
    decreases steps;
{
    if steps > 0 then
        stepMany(i + 1,steps - 1)
    else
        i
}

lemma ex2()
{
    ghost var ex1 := 10;
    ghost var ex1Done := stepMany(ex1,33);
    assert ex1Done == 43; // assertion verifies successfully
}

但是，以下代码无法验证：

function stepMany(i : int,34);     <-- only differences here
    assert ex1Done == 44;                       <-- and here
    // assertion DOES NOT verify
}

唯一的区别是stepMany的第二个参数。该断言适用于所有多达33个参数，而对于超过34个的所有参数均无效。

Dafny是否可以处理最多数量的递归调用？我尝试搜索文档，但一无所获。似乎有一个命令行参数“ / recursionBound”，但它不会影响结果。

解决方法

此限制不是在递归级别上，而是在展开级别上。当Dafny具有递归定义时，它将稍稍展开。但并非没有限制。

您想要的是让Dafny意识到stepMany只是一个添加函数。一种方法是编写引理。然后，您需要通过调用引理来提醒Dafny您所讲的内容。像这样：

// Hey Dafny,the stepMany functions adds its arguments and returns the result.
lemma stepManyAddsItsArguments(i : int,steps : int)
requires steps >= 0
ensures stepMany(i,steps) == i+steps
decreases steps 
{} // Hey Dafny,would you mind proving that?

lemma ex2()
{
    ghost var ex1 := 10;
    ghost var ex1Done := stepMany(ex1,34);
    stepManyAddsItsArguments( ex1,34) ; // Heh Dafny,remember what I told you about stepMany!
    assert ex1Done == 44;
}