Information Technology Reference
In-Depth Information
case
Cons(h1, t1 @ Cons(h2, t2))
⇒
(h1
≤
h2)
&&
isSorted(t1)
case
⇒
true
}
Thanks to the abstraction function and the invariant, we can concisely specify
an
insert
operation for sorted lists using a constraint:
def
insert(l: List, v: Int) =
{
require
(isSorted(l))
choose
{
(x: List)
⇒
isSorted(x)
&&
(content(x)
==
content(l)
++
Set(v))
}
}
Our deductive synthesis procedure is able to translate this constraint into the
following complete implementation in under 9 seconds:
def
insert(l: List, v: Int) =
{
require
(isSorted(l))
l
match
{
case
Cons(head, tail)
⇒
if
(v
==
head)
{
l
}
elseif (v
<
head)
{
Cons(v, l)
}
else
{
insert(t, v)
}
case
Nil
⇒
Cons(v, Nil)
}
}
However, as the complexity of the constraints increases, the deductive procedure
may run short of available time to translate a constraint into complete ecient
implementations. As an example, we can currently observe this limitation of
our system for a red-black tree benchmark. The following method describes the
insertion into a red-black tree.
1
def
insert(t: Tree, v: Int) =
{
require
(isRedBlack(t))
choose
{
(x: Tree)
⇒
isRedBlack(x)
&&
(content(x)
==
content(t)
++
Set(v))
}
}
Instead of using synthesis (for which this example may present a challenge), we
can rely on the run-time constraint solving to execute the constraint. In such
scenario, the run-time waits until the argument
t
and the value
v
are known,
and finds a new tree value
x
such that the constraint holds. Thanks to our
constraint solver, which has a support recursive functions and also leverages
the Z3 SMT solver, this approach works well for small red-black trees. It is
therefore extremely useful for prototyping and testing and we have previously
1
We omit here the definition of the tree invariant for brevity, which is rather complex
[15,52], but still rather natural to describe using recursive functions.
