是否可以根据规范而不是实现来推理？

Question

我想在不知道具体实现的情况下使用 Leon 来验证规范。例如，假设我有一个排序函数，以及排序列表的定义：

def sort (list: List[BigInt]): List[BigInt] = {
    ...
  } ensuring {
    res => res.content == list.content && isSorted(res)
  }

def isSorted (list: List[BigInt]): Boolean = {
    list match {
      case Nil()                  => true
      case Cons(_, Nil())         => true
      case Cons(x1, Cons(x2, xs)) => x1 <= x2 && isSorted(list.tail)
    }
  }

理想情况下，我应该能够根据sort单独的post条件证明诸如sort(sort(list)) == sort(list)的引理。否则，我不能声称适用于插入排序的 Leon 证明也适用于快速排序（实际上很少这样做）。 Leon 是否可以在不查看实现的情况下根据前提条件和 post 条件进行推理？

谢谢！

Answer 1

使用 xlang 扩展（在命令行上使用 --xlang，并在 Web 界面中默认支持），您可以访问带有谓词和 return一个满足它的表达式。有了它你基本上可以省略代码中一些功能的实现。你的例子可以写成：

import leon.lang._
import leon.collection._
import leon.lang.xlang._

object Test {
  def isSorted(l: List[BigInt]): Boolean = l match {
    case Nil() => true
    case Cons(x, Nil()) => true
    case Cons(x, Cons(y, ys)) => x <= y && isSorted(l.tail)
  }
  def sort(l: List[BigInt]): List[BigInt] = epsilon((o: List[BigInt]) =>
    l.content == o.content && isSorted(l))
  def prop1(l: List[BigInt]): Boolean = {
    sort(sort(l)) == sort(l)
  } holds
}

哪个做你想要的。然而上面的属性 prop1 是无效的，Leon 会告诉你。问题是 sort 的规范只保证相同的内容，但不检查重复项。因此，sort 的实现行为如下：

是有效的

sort(List(1)) == List(1, 1)

因此你可以得到：

sort(sort(List(1))) == List(1, 1, 1) != sort(List(1))

但是，如果您找到使 sort 的后置条件更强的方法，那么您应该能够使用上述方法来验证规范。当然，如果你有一个不同于 sort 的例子，你可以使用 epsilon 没有任何问题，只是要注意 under-specification 的问题。

是否可以根据规范而不是实现来推理？

Is it possible to reason based on spec instead of the implementation?

leon