3 ms·
Looking at this example[1]: def size(l: List) : Int = (l match { case Nil => 0 case Cons(_, t) => 1 + size(t) }) ensuring(res =
by hello_there 12y ago
Looking at this example[1]:
def size(l: List) : Int = (l match {
case Nil => 0
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
What happens if the length of the list is greater than `Int.MaxValue`? Reading the part of the code that says `ensuring(res => res >= 0)` I would expect that it checked for overflow, but I don't understand what prevents this from overflowing, especially since the case classes that define the list are public and as a consequence I may create arbitrarily long lists.
Am I missing something?
[1]: http://leon.epfl.ch/#link/bb8d258a234aaeb380d9e1c46aa60b13-1 http://leon.epfl.ch/#link/bb8d258a234aaeb380d9e1c46aa60b13-1
- psuter 12y agoGood catch. Leon indeed currently models the `Int` type as mathematical (unbounded) integers. There is a project in the works to correct this semantic difference with Scala, and have `Int` be signed 32-bit bitvectors and `BigInt` be the mathematical integers. At that stage, Leon will also be able to generate the kind of bound checks you were expecting. For the types of problems we had been looking at, the current state is arguably not a major issue (if you are really building a list of 2^31 elements, you're probably facing other problems), but for the sake of being formal, the semantic mismatch must be addressed.