leon - Leon 无法证明简单递归程序的正确性？

Question

我曾尝试在 Leon 进行以下程序

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）并且必须展开公式直到它到达溢出。当然，最好只找到反例并报告它，但由于 Leon 使用的算法，这是一个限制。

请注意，您的第一个程序是valid因为永远不会溢出。