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)
}
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.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With