Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to prove size of a list in Leon?

Tags:

scala

leon

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)
}
like image 706
vkuncak Avatar asked Apr 23 '15 18:04

vkuncak


1 Answers

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.

like image 116
Philippe Avatar answered Sep 20 '22 21:09

Philippe