Information Technology Reference
In-Depth Information
both how the subproblem relates to the original one, and how its solution and
precondition are used in the final program.
Another example is the following rule for decomposing disjunctions:
T
1
T
2
a
Π
φ
1
x
P
1
|
a
Π
∧¬
P
1
φ
2
x
P
2
|
T
1
}
T
2
}
a
Π
φ
1
∨
φ
2
x
P
1
∨
P
2
|
if(
P
1
)
{
else
{
Here, the rule states that a disjunction can be handled by considering each
disjunct in isolation, and combining the solutions as an if-then-else expression,
where the branching condition is the precondition for the first problem. Note that
in the second subproblem, we have added the literal
P
1
to the path condition.
This reflects the knowledge than, in the final program, the subprogram for the
second disjunct only executes if the first one cannot compute a solution.
In general, a synthesis problem is solved whenever a derivation can be found
for which all output variables are assigned to a program term.
For certain well-defined classes of synthesis problems, we can design sets of
inference rules which, together with a systematic application strategy, are guar-
anteed to result in successful derivation. We have shown in previous work such
complete strategies for integer linear arithmetic, rational arithmetic, or term
algebras [32,40,67]. We call these
synthesis procedures
, analogously to decision
procedures.
As a final example, we now show how our framework can express solutions
that take the form of recursive functions traversing data structures. The next
rule captures one particular yet very common form of such a traversal for Lists.
(
Π
1
∧P
)=
⇒ Π
2
¬
Π
2
[
a
0
→
Cons
(
h,t
)] =
⇒ Π
2
[
a
0
→ t
]
T
1
a
Π
2
φ
[
a
0
→
Nil
]
x
|
T
2
r,h,t,a
Π
2
[
a
0
→
Cons
(
h,t
)]
∧
φ
[
a
0
→
t, x
→
r
]
φ
[
a
0
→
Cons
(
h,t
)]
x
|
a
0
,a
Π
1
φ
x
P
|
rec
(
a
0
,a
)
The goal of the rule is to derive a solution consisting of a single invocation of
a (fresh) recursive function
rec
, of the following form:
def
rec(
a
0
,
a
)=
{
require
(
Π
2
)
a
0
match
{
case
Nil
⇒
T
1
case
Cons(
h
,
t
)
⇒
val
r
=rec(
t
,
a
)
T
2
}
}
ensuring
(
r ⇒ φ
[
x → r
]
)
The rule decomposes the problem into two cases, corresponding to the alterna-
tives in the data type, and assumes that the solution takes the form of a
fold
function, fixing the recursive call.
