For the verification part, the main paper is "Satisfiability Modulo Recursive Programs", SAS 2011 [1]. For the synthesis part, the most up-to-date paper is "Synthesis Modulo Recursive Functions", OOPSLA 2013 [2]. As is usual with CS papers, searching for the title in your favorite search engine may or may not help you find a PDF version.
I'm an author on both papers, so feel free to ask any questions here as well.
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.
Good 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.
5 comments
[ 4.4 ms ] story [ 20.9 ms ] threadI'm an author on both papers, so feel free to ask any questions here as well.
[1] http://link.springer.com/chapter/10.1007%2F978-3-642-23702-7...
[2] http://dl.acm.org/citation.cfm?id=2509555
Am I missing something?
[1]: http://leon.epfl.ch/#link/bb8d258a234aaeb380d9e1c46aa60b13-1
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.