Information Technology Reference
In-Depth Information
explored it as a stand-alone technique for constraint programming in Scala [39].
However, the complexity of reasoning symbolically about complex trees makes
this approach inadequate for large concrete inputs.
Fortunately, thanks to the nature of our deductive synthesis framework, we
can combine synthesis and run-time constraint solving. We illustrate this using
an example of a
red-black tree with a cache
. Such a tree contains a red-black tree,
but also redundantly stores one of its elements.
case class
CTree(cache: Int, data: Tree)
The specification of the invariant
inv
formalizes the desired property: the cache
value must be contained in the tree unless the tree is empty.
def
inv(ct: CTree) =
{
isRedBlack(ct.data)
&&
(ct.cache
∈
content(ct.data))
||
(ct.data
==
Empty)
}
The
contains
operation tests membership in the tree.
def
contains(ct: CTree, v: Int): Boolean =
{
require
(inv(ct))
choose
{
(x: Boolean)
⇒
x
==
(v
∈
content(ct))
}
}
While not being able to fully translate it, the deductive synthesis procedure
decomposes the problem and partially synthesizes the constraint. One of its
possible results is the following
partial
implementation that combines actual
code and a sub-constraint:
def
contains(ct: CTree, v: Int): Boolean = ct.data
match
{
case
n: Node
⇒
if
(ct.cache
==
v)
{
true
}
else
{
choose
{
(x: Boolean)
⇒
x
==
(v
∈
content(n))
}
}
case
Empty
⇒
false
}
We notice that this partial implementation makes use of the cache in accordance
with the invariant. The code accurately reflects the fact that the cache may not
be trusted if the tree is empty. The remaining constraint is in fact a simpler
problem that only relates to standard red-black trees. Our system can then
compile the resulting code, where the fast path is compiled as the usual Scala
code, and the
choose
construct is compiled using the run-time solving approach.
In the sequel we give details both for our run-time solving approach and the
compile-time deductive synthesis transformation framework. We then discuss
our very first experience with combining these two approaches.
