如何证明 Leon 中列表的大小？

Question

我试图证明列表中的大小（元素数量）是非负的，但 Leon 未能证明它——它只是超时了。这个属性是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 的 return 类型更改为 BigInt，程序将按预期进行验证。

Answer 2

前面的答案都对，但如果我们希望使用 Int 而不是 BigInt 并且感觉合理列表的大小是非负的，则对我们没有帮助。以下简单的技巧可以解决这个问题并适用于不锈钢：

def listLength(l: List[T]): Int = {
    l match {
        case head :: tl => {
            val tlLen = listLength(tl)
            if(tlLen < Int.MaxValue) {
                tlLen + 1
            } else {
                0
            }
        }
        case Nil() => 0
    }
} ensuring(0 <= _)

参见，例如，https://github.com/epfl-lara/bolts/blob/master/data-structures/seqs/ArrayList.scala in the bolts repository of https://stainless.epfl.ch/

如何证明 Leon 中列表的大小？

How to prove size of a list in Leon?

scala

leon