Frequently Asked Questions

If you have a question, we suggest you post it at http://stackoverflow.com (try searching for the leon tag) or contact one of the authors of this documentation.

Below we collect answers to some questions that came up.

Proving properties of size

I have defined a size function on my algebraic data type.

sealed abstract class List
case class Cons(head: Int, tail: List) extends List
case object Nil extends List
def size(l: List) : Int = (l match {
  case Nil => 0
  case Cons(_, t) => 1 + size(t)
}) ensuring(_ >= 0)

Leon neither proves nor gives a counterexample. Why?

Answer: You should consider using BigInt, which denotes unbounded mathematical integers, instead of Int, which denotes 32-bit integers. If you replace Int with BigInt in the result type of size, the function should verify. Note that algebraic data types can be arbitrarily large, so, if the input list had the size Int.MaxValue + 1 (which is 2^32) then the addition 1 + size(t) would wrap around and produce Int.MinValue (that is, -2^31), so the ensuring clause would not hold.

Use variable number of arguments in Leon programs

I have defined an apply function that should accept a variable number of arguments.

import leon.collection._
case class Element(children: List[Element]) {
  def addChildren(c: Element*): Element = {
    Element(children ++ c.toList)
  }
}

This does not compile in Leon, why?

Answer:

To support variable number of arguments, do the following:

import leon.collection._
import leon.annotation._
case class Element(children: List[Element]) {
  @ignore
  def addChildren(c: Element*): Element = {
    var l: List[WebTree] = Nil[WebTree]()
    for (e <- elems) {
      l = Cons(e, l)
    }
    addChildren(l.reverse)
  }
  def addChildren(c: List[Element]): Element = {
    Element(children ++ toList)
  }
}

This code is compatible with both Leon and Scala. At parsing time, when Leon encounters a call to addChildren(a, b) using the first method, it translates it to addChildren(Cons(a, Cons(b, Nil()))) using the second method. When Scala encounters the same call, it executes the @ignore-d function and calls the second method.

The reason is that the scala.collection.Seq used in the case of multiple arguments does not have a method toList that converts the sequence to a Leon List. Hence this workaround.

Compiling Leon programs to bytecode

If you don’t use special constructs such as choose, you should be able to compile Leon programs to .class using scalac and execute them directly on the JVM, or integrate them as part as other Scala-based projects.

Beware that you need to explicitly include files files from the Leon library (that are implicitly bundled when you use the ./leon script):

$ mkdir out
$ scalac $(find path/to/leon/library/ -name "*.scala" | xargs) MyFile.scala -d out