Information Technology Reference
In-Depth Information
data structure, we implemented a declarative version of the
add
and
remove
operations. Thanks to the abstraction and predicate functions, the specifications
of both operations are very concise and self-explanatory. We illustrate this by
providing the corresponding code for red-black trees:
def
add(t: Tree, e: Int): Tree = choose
{
(res: Tree)
⇒
content(res)
==
content(t)
++
Set(e)
&&
isRedBlackTree(res)
}
def
remove(t: Tree, e: Int): Tree = choose
{
(res: Tree)
⇒
content(res)
==
content(t)
--
Set(e)
&&
isRedBlackTree(res)
}
Solving is relatively ecient for small data structures: it finds models in under
400ms for lists and trees up to size 4. However, the necessary solving time in-
creases exponentially with the size and goes as high as 35 seconds for synthesizing
insertion into a red-black tree of size 10.
5 Synthesizing Functional Code from Constraints
In this section, we give an overview of our framework for deductive synthesis.
The goal of the approach is to derive correct programs by successive steps. Each
step is validated independently, and the framework ensures that composing steps
results in global correctness.
5.1 Synthesis Problems and Solutions
A synthesis problem, or constraint, is fundamentally a relation between in-
puts and outputs. We represent this, together with contextual information, as a
quadruple
a
Π
φ
x
where:
-
a
denotes the set of
input variables
,
-
x
denotes the set of
output variables
,
-
φ
is the
synthesis predicate
,and
-
Π
is the
path condition
to the synthesis problem.
The free variables of
φ
must be a subset of
a
x
. The path condition denotes
a property that holds for input at the program point where synthesis is to be
performed, and the free variables of
Π
should therefore be a subset of
a
.
As an example, consider the following call to
choose
:
∪
def
f(a : Int) : Int =
{
if
(a
≥
0)
{
choose((x : Int)
⇒
x
≥
0
&&
a+x
≤
5)
}
else
...
}
