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で修正する必要があります。

これは、型推論が、宣言された戻り値の型から untyped を介してensuring関数の本体まで型を追跡できないことが原因でした。これによりNil()、本体で不正確に型付けされ、型のないクロージャーが拒否されます。

これが Leon 内で機能したのはなぜですか? パターンが

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

Leon プログラムでは頻繁に使用されます。

于 2015-05-03T19:26:07.023 に答える
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 に答える