1

我正在尝试直接使用 scalac 编译我的 Leon 代码。不幸的是，我无法正确构建代码所依赖的 Leon 库。

例如，我跑了

scalac $(find ~/my-path/leon/library/ -name "*.scala" | xargs) Queue.scala

但这实际上会返回错误：

.../leon/library/collection/List.scala:81: error: missing parameter type for expanded function ((x$2) => x$2.size.$eq$eq(if (i.$less$eq(0))
  BigInt(0)
else
  if (i.$greater$eq(this.size))
    this.size
  else
    i))
  }} ensuring { _.size == (
                ^

应该将什么传递给 scalac 以避免库中的这些错误并最终编译我自己的源文件？

谢谢！

4

3 回答 3

3

首先，我怀疑这里的尝试是执行 Leon 程序，如果是这样，有一个名为的新选项将评估所有地面功能（您可以像往常一样--eval进一步过滤它）。--functions这应该可以防止骨架实现无法执行的问题。

关于编译问题：现在应该在https://github.com/epfl-lara/leon/commit/3d73c6447916516d0ad56806fe0febf7b30a71ad中修复

这是由于类型推断无法跟踪从声明的返回类型到 untypedensuring到函数体的类型。这会导致Nil()在正文中输入不精确，进而导致无类型闭包被拒绝。

为什么这在 Leon 内部起作用？Leon 在类型检查之前在 Scala 编译器管道中插入一个阶段，以注入使这种推断成为可能（并且方便）的提示，因为模式

def foo(a: A): B = { a match {
   case ..
   case ..
}} ensuring { .. }

在 Leon 程序中如此频繁。

于 2015-05-03T19:26:07.023 回答
1

奇怪的是，写这样的东西：

def take(i: BigInt): List[T] = { val res: List[T] = (this, i) match {
    case (Nil(), _) => Nil()
    case (Cons(h, t), i) =>
      if (i <= BigInt(0)) {
        Nil()
      } else {
        Cons(h, t.take(i-1))
      }
  }; res} ensuring { _.size == (
    if      (i <= 0)         BigInt(0)
    else if (i >= this.size) this.size 
    else                     i
  )}

...使其清楚明确。Scalac 无法推断出正确的参数类型，但这使得第一个块的返回类型足够明确。但是请注意，直接使用 Leon 不是问题，这是整个 Leon 库中使用的通用语法，而不是我的代码。

通过更改上面解释的所有函数，我能够编译 Leon 库 - 但不能使用正常的 scala 语法运行项目，因为在https://github.com/epfl-lara/leon/blob/master/中设置了实现不知何故，Leon 没有使用library/lang/Set.scala，它丢失了。

于 2015-05-03T14:11:35.093 回答
0

跟随艾蒂安的帖子：

这可行，但我们仍然需要在https://github.com/epfl-lara/leon/blob/master/library/lang/Set.scala中实现集合。我是这样做的：

package leon.lang
import leon.annotation._
import scala.collection.{ immutable => imm }

object Set {
  @library
  def empty[T] = Set[T]()
  protected[Set] def apply[T](elems: imm.Set[T]): Set[T] = Set(elems.toSeq :_*)
}

@ignore
case class Set[T](elems: T*) {
  def +(a: T): Set[T] = Set(elems.toSet + a)
  def ++(a: Set[T]): Set[T] = Set(elems.toSet ++ a.elems.toSet) //Set.trim(elems ++ a.elems) //Set((elems.toSeq ++ a.elems.toSeq).toSet.toSeq :_*)
  def -(a: T): Set[T] = Set(elems.toSet - a)
  def --(a: Set[T]): Set[T] = Set(elems.toSet -- a.elems.toSet)
  def contains(a: T): Boolean = elems.toSet.contains(a)
  def isEmpty: Boolean = this == Set.empty
  def subsetOf(b: Set[T]): Boolean = elems.toSet.forall(e => b.elems.toSet.contains(e))
  def &(a: Set[T]): Set[T] = Set(elems.toSet & a.elems.toSet)
}

不幸的是，这不能像在 Leon 中那样直接使用：

[ Error  ] 8:31: Scala's Set API is no longer extracted. Make sure you import leon.lang.Set that defines supported Set operations.
         protected[Set] def apply[T](elems: imm.Set[T]): Set[T] = Set(elems.toSeq :_*)
                                     ^^^^^^^^^^^^^^^^^

但它适用于编译scalac和运行scala使用：

scalac $(find ~/my-path/leon/library/ -name "*.scala" | xargs) Queue.scala

无论如何，如果--eval成功了，让我们使用它吧！

谢谢！

于 2015-05-04T10:10:38.503 回答