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

发布时间：2020-12-16 19:13:40 所属栏目：安全来源：网络整理

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

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

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

解决方法

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

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

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

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!