3

我有一个抽象的堆栈类型如下

abstract class Stack[T] {
  def empty  : Stack[T]
  def pop () : (Option[T], Stack[T])
  def push (e : T) : Stack[T]
  def size : BigInt
}

我想验证pop返回最后推送的元素：

// ok
def test_v1[T] (e : T, s : Stack[T]) : Boolean = {
  s.push(e).pop()._1 match {
    case Some(e2) => e == e2
    case _        => false
  }
} holds

// failed
def test_v2[T] (e : T, s : Stack[T]) : Boolean = {
  s.push(e).pop()._1 == Some(e)
} holds

这两个引理是等价的，但 Leon 无法识别第二个引理中的类型参数。Stack有趣的是，Leon 在具体或非泛型时都没有问题 （请参阅下面的链接以获取示例）。这是 Leon 的功能还是只是一个错误？

完整的示例代码可以在这里找到。

4

1 回答 1

1

我在您的 gist 链接中尝试了该示例（在“可以在此处找到”下），它适用于当前版本的 Leon，在线和 git 存储库中。所以，如果这是一个错误，它现在被修复了。如果您有任何相关问题，我们很乐意回答，因为 Leon 目前仅支持对象和案例类，因此与完整的 Scala 相比存在差异。

于 2016-03-14T16:04:20.007 回答