Leon – An Automated System for Synthesizing and Verifying Scala Programs

Here are some resources on Leon, including github link, videos of talks, and more papers: http://lara.epfl.ch/w/leon

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

Where's the paper? :)