Information Technology Reference
In-Depth Information
the remedial action in case of assertion violation [57]. However, we believe that
such constructs should not be treated as a sort of exception mechanism, but as
one of the main ways of describing the desired common behavior.
This paper presents our experience in developing techniques to make such
constraint solving executable. Our current approach combines deductive syn-
thesis with run-time constraint solving, in both cases leveraging modern SMT
solvers. We have built a tool as part of the Leon verification system [9] that
incorporates both techniques and allows us to experiment with their trade-offs.
A version of the Leon platform is publicly available in source code form for fur-
ifications into simpler fragments using a cost-driven deductive synthesis frame-
work [32,37,40-42]. It compiles as many fragments as possible into conventional
functional code; it executes the remaining fragments by invoking a constraint
solver at runtime. The solver extends a conventional SMT solver with the ability
to handle recursive functions, in a manner similar to our previous systems [38,39].
Using this approach we were able to execute constraints that describe the desired
properties of integers, sets, maps and algebraic data types.
In general, the deductive synthesis framework allows us to recursively split
challenging problems into tractable subproblems and compile some of the sub-
problems into conventional code. If a subproblem remains too challenging for
synthesis, we keep its declarative specification and execute it using run-time
constraint solving. It turns out that in certain interesting cases, the resulting
partial program is well-defined for simple, frequent paths and only relies on
run-time constraint solving for complex cases.
In the rest of this paper we outline our approach, including the functional lan-
guage setup, the run-time constraint solving approach, and synthesis techniques.
We then illustrate our initial experience with combining run-time constraint solv-
ing and synthesis, hinting at some future directions. We finish with a (necessary
biased) survey of related work.
2 Examples
We illustrate the benefits of enabling declarative specifications through a series
of examples. We show how these examples can be effectively handled by our
system. We start by defining a List data-structure with an abstraction function
content
from list to a set, and an invariant predicate
isSorted
.
abstract class
List
case class
Cons(head: Int, tail: List)
extends
List
case object
Nil
extends
List
def
content(l: List): Set[Int] = l
match
{
case
Cons(h, t)
⇒
Set(h)
++
content(t)
case
Nil
⇒
Set()
}
def
isSorted(l: List): Boolean = l
match
{
