证明有序列表的串联是不锈钢中的有序列表

Question

我有以下用于排序数组的代码，我想在 Stainless（以前称为 Leon）中进行验证：

import stainless.lang._
import stainless.collection._

object QuickSort {

  def isSorted(list: List[BigInt]): Boolean = list match {
    case Cons(x, xs @ Cons(y, _)) => x <= y && isSorted(xs)
    case _ => true
  }

  def quickSort(list: List[BigInt]): List[BigInt] = (list match {
        case Nil() => Nil[BigInt]()
        case Cons(x, xs) => par(x, Nil(), Nil(), xs)
  }) ensuring { res => isSorted(res) }


  def par(x: BigInt, l: List[BigInt], r: List[BigInt], ls: List[BigInt]): List[BigInt] = {
    require(l.forall(_ <= x) && r.forall(_ >= x))
    ls match {
      case Nil() => quickSort(l) ++ Cons(x, quickSort(r))
      case Cons(x2, xs2) => if (x2 <= x) par(x, Cons(x2, l), r, xs2) else par(x, l, Cons(x2, r), xs2)
    }
  } ensuring {res => isSorted(res)}
}

我有很多方向可以从这里开始（因为它没有成功验证）但是在我看来，根据提供的提示验证应该成功，我想知道为什么它没有。我自己解释一下：

显然为了验证 par 函数，我需要证明这两种情况分别隐含了 isSorted 后置条件。现在，由于第二种情况包含递归调用，因此很明显它暗示了后置条件。对于 par 的第一种情况，我们对左右子数组进行了排序，前提条件告诉我所有元素都相对于主元进行了排序。

最后一点在我看来应该意味着串联列表也已排序。那为什么不验证呢？如何指示不锈钢来验证它？我是否需要添加有关长度和尺寸的提示以方便不锈钢的任务？

编辑：

def concatIsSorted(l1 : List[BigInt],l2 : List[BigInt],pivot : BigInt) : Boolean = {
    require(isSorted(l1) && isSorted(l2) && l1.forall(_ <= pivot) && l2.forall(_ >= pivot))
    isSorted(l1 ++ Cons(pivot,l2)) because{
      l1 match{
        case Nil() => isSorted(Cons(pivot,l2))
        case Cons(h,Nil()) => h <= pivot && isSorted(Cons(pivot,l2))
        case Cons(h,t) => h <= t.head && concatIsSorted(t,l2,pivot)
      }     
    }   
  }.holds

Answer 1

因为这是一道looks like家庭作业题，我会尽量引导你找到解决方案而不泄露它。

首先请注意，程序会验证您是否将 par 中的 Nil() 大小写替换为 case Nil() => Nil()。这表明验证者无法证明 quickSort(l) ++ Cons(x, quickSort(r)) 的结果已排序（但它设法为 Nil() 做到了！）。

当--debug=verification不足以理解为什么验证者不能证明你认为它应该证明时，继续的方法是引入额外的功能，你可以在其中准确地表达你的期望。例如，如果您定义：

def plusplus(l: List[BigInt], r: List[BigInt]): List[BigInt] = l ++ r

并用您希望验证者证明的内容对其进行注释，即

假设 l 和 r 已排序并且 l < r（对于 < 的适当定义）
l ++ r的结果排序

你会看到验证者无法证明这个属性，这意味着你需要通过额外的辅助功能，前置条件和后置条件来进一步指导验证。

请注意，此示例取自 Dependent Types for Program Termination Verification，阅读本文可能会对您有所帮助。

证明有序列表的串联是不锈钢中的有序列表

Proof the concatenation of ordered list is an ordered list in Stainless

formal-verification

scala

stainless