如何证明莱昂的名单大小？

Question

我试图证明列表中的大小(元素数量)是非负的,但莱昂未能证明它 - 它只是超时.莱昂真的没有能力证明这个属性,还是我错误地使用它？我的出发点是我在文章"莱昂验证系统概述"中读到的一个功能.

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,这是一个反例,它将证明后置条件不适用于有界整数.

如果更改sizeto 的返回类型BigInt,程序将按预期进行验证.