Leon不能证明简单递归程序的正确性？

Question

我在里昂尝试过以下节目

object Test10 {

     def sum(n: Int): Int = ({ 
        require(n >= 0)
        if (n == 0) 0
        else    sum(n-1)+1
    })ensuring(res => res==n )    

}

结果-成功

object Test10 {

     def sum(n: Int): Int = ({ 
        require(n >= 0)
        if (n == 0) 0
        else    sum(n-1)+n
    })ensuring(res => res==n*(n+1)/2 )

 }

结果-失败(未终止)

我是否犯了什么错误，为什么系统不能产生?有人能引导我吗？

Answer 1

第二个程序实际上不是valid。由于溢出，对于n的大值，后置条件是不正确的。当总和溢出时，公式将不再成立。

您可以尝试将Int替换为BigInt，它可能会工作。由于非线性算法的存在，该问题也很难解决。

Leon没有终止，因为它正在寻找一个反示例(因为程序不是valid)，并且必须展开公式直到它到达溢出。当然，最好只是找到反例并报告它，但这是一个限制，因为莱昂使用的算法。

请注意，您的第一个程序是valid，因为从来没有溢出。