faq.rst

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.