7

我试图证明列表中的大小（元素数量）是非负的，但 Leon 未能证明这一点——它只是超时了。Leon 真的无法证明这个属性，还是我用错了？我的出发点是我在“Leon 验证系统概述”一文中读到的一个函数。

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)
}
4

2 回答 2

6

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

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

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

于 2015-04-23T18:26:00.630 回答
0

以前的答案是正确的，但如果我们希望使用 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://stainless.epfl.ch/的螺栓存储库中的https://github.com/epfl-lara/bolts/blob/master/data-structures/seqs/ArrayList.scala

于 2021-05-02T12:59:55.103 回答