7

I am trying to prove that the size (number of elements) in a list is non-negative, but Leon fails to prove it---it just times out. Is Leon really not capable of proving this property, or am I using it wrongly? My starting point is a function I read in the paper "An Overview of the Leon Verification System".

import leon.lang._
import leon.annotation._

object ListSize {
  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)
}
Philippe
  • 9,582
  • 4
  • 39
  • 59
vkuncak
  • 123
  • 7

2 Answers2

6

Previous versions of Leon treated Scala's Int type as mathematical, unbounded, integers. The most recent versions treat values of Int as signed 32-bit vectors, and require the use of BigInt to represent unbounded integers.

In the provided example, Leon times out attempting to build a list of size Int.MaxValue, a counter-example which would demonstrate that the postcondition does not hold for bounded integers.

If you change the return type of size to BigInt, the program verifies as expected.

Philippe
  • 9,582
  • 4
  • 39
  • 59
  • But why don't I get a counter-example to tbe program with Int? – vkuncak Apr 26 '15 at 15:55
  • Leon searches for counter-examples by (conceptually) enumerating structures of increasing size. The smallest counter-example to this verification condition has size `Int.MaxValue`, so it'll take some time to get there (and you'll run out of memory before). – Philippe Apr 27 '15 at 17:55
0

Previous answers are all right, but do not help us if we wish to use Int instead of BigInt and have a sense that the size of reasonable lists is non-negative. The following simple trick takes care of that and works in stainless:

def listLength(l: List[T]): Int = {
    l match {
        case head :: tl => {
            val tlLen = listLength(tl)
            if(tlLen < Int.MaxValue) {
                tlLen + 1
            } else {
                0
            }
        }
        case Nil() => 0
    }
} ensuring(0 <= _)

See, for example, https://github.com/epfl-lara/bolts/blob/master/data-structures/seqs/ArrayList.scala in the bolts repository of https://stainless.epfl.ch/

vkuncak
  • 123
  • 7