1

我想在事先不知道具体实现的情况下使用 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(sort(list)) == sort(list)基于sort 单独的后置条件。否则，我不能声称适用于插入排序的 Leon 证明也适用于快速排序（实际上很少这样做）。Leon 是否有可能在不研究实现的情况下根据前置条件和后置条件进行推理？

谢谢！

4

1 回答 1

2

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

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毫无问题地使用，只要注意规格不足的问题。

于 2015-09-05T14:02:25.740 回答