scala - 如何证明莱昂列表的大小？

Question

我试图证明列表中的大小(元素数量)是非负数，但 Leon 未能证明这一点——它只是超时了。莱昂真的没有能力证明这个性质，还是我错误地使用了它？我的出发点是我在论文“An Overview of the Leon Verification System”中读到的一个函数。

import leon.lang._
import leon.annotation._

object ListSize {
  sealed abstract class List
  case class Cons(head: Int, tail: List) extends List
  case object Nil extends List

  def size(l: List) : Int = (l match {
    case Nil => 0
    case Cons(_, t) => 1 + size(t)
  }) ensuring(_ >= 0)
}

Answer 1

Leon 的早期版本将 Scala 的 Int 类型视为数学、无界整数。最新版本将 Int 的值视为带符号的 32 位向量，并要求使用 BigInt 来表示无界整数。

在提供的示例中，Leon 在尝试构建大小为 Int.MaxValue 的列表时超时，这是一个反例，它将证明后置条件不适用于有界整数。

如果将 size 的返回类型更改为 BigInt，程序将按预期进行验证。