Information Technology Reference
In-Depth Information
The representation of the corresponding synthesis problem is:
a a ≥
0
x ≥
0
∧a
+
x ≤
5
x
(1)
T
We represent a solution to a synthesis problem as a pair
P
|
where:
-
P
is the
precondition
,and
-
T
is the
program term
.
The free variables of both
P
and
T
must range over
a
. The intuition is that,
whenever the path condition and the precondition are satisfied, evaluating
φ
[
x
→
T
] should evaluate to
(true), i.e.
T
are realizers for a solution to
x
in
φ
given the
inputs
a
. Furthermore, for a solution to be as general as possible, the precondition
must be as weak as possible.
Formally, for such a pair to be a solution to a synthesis problem, denoted as
T
a
Π
φ
x
P
|
the following two properties must hold:
T
]
This property states that whenever the path- and precondition hold, the
program
T
can be used to generate values for the output variables
x
such
that the predicate
φ
is satisfied.
-
Domain preservation:
Π
-
Relation refinement:
Π
∧
P
|
=
φ
[
x
→
=
P
This property states that the precondition
P
cannot exclude inputs for which
an output exists.
∧
(
∃
x
:
φ
)
|
As an example, a valid solution to the synthesis problem (1) is given by:
5 characterizes exactly the input values for
which a solution exists, and for all such values, the constant 0 is a valid solution
term for
x
. The solution is in general not unique; alternative solutions for this
particular problem include
a
≤
5
|
0
. The precondition
a
≤
a
≤
|
−
a
a
≤
|
if
(
a<
5)
a
+1
else
0
5
5
,or
5
.
5.2 Inference Rules
The correctness conditions described above characterize the validity of solutions
to synthesis problems. We now show how to derive such solutions. We present
our techniques as a set of
inference rules
. As a simple first example, consider the
following rule:
T
a
Π
φ
[
x
0
→
t
]
x
P
|
x
0
/
∈
vars(
t
)
val
x
:=
T
;
(
t,x
)
a
Π
x
0
=
t
∧
φ
x
0
, x
P
|
As is usual with inference rules, on top are the premisses and below is the goal.
This particular rule captures the intuition that, whenever a term of the form
x
0
=
t
appears as a top-level conjunct in a synthesis problem, the problem can
be simplified by assigning to the output variable
x
0
the term
t
. The rule specifies
