Information Technology Reference
In-Depth Information
Partial evaluation is used in [21] to generate test cases and test case genera-
tors for given target programs. Instead of using a dedicated symbolic execution
engine, they use partial evaluation to obtain an executable version of the imple-
mentation under test in the language CLP. CLP programs can then be executed
on symbolic values returning a set of constraints on those input values. Par-
tial evaluation is used as an approximation and replacement for a fully precise
symbolic execution engine while we are interested in using partial evaluation to
speed up symbolic execution in a dedicated symbolic execution engine.
There is a close relationship between the rule for specialization operator prop-
agation (SOP) in Sect. 4.3 and what is known as
binding time analysis
(BTA)
in partial evaluation. Partial evaluation techniques roughly categorize program
variables into those which are known to have a constant value independent from
any input and those whose value may vary. BTA in partial evaluation determines
to which of these categories a variable belongs to. The precision of the analysis
has a significant impact on the power of partial evaluation as too early binding
prevents certain optimizations. The modifier set
mod
in the SOP rule influences
directly the precision of the BTA performed by our specialization operator. If
the oracle determining
mod
is too conservative (imprecise) too much knowledge
of the current state
U
will be lost and cannot be utilized in later specializations.
8 Conclusions and Future Work
In this paper we concentrated on deductive program verification as the main
application scenario, however, as pointed out in Sect. 2.2, symbolic execution has
other important usages, such as automatic test case generation [10,9]. It would
be interesting to investigate whether partial evaluation can lead to a reduction
of redundant test cases.
We showed that a fairly na ıve partial evaluator can be used to boost perfor-
mance of a symbolic execution engine. In Sect. 7 we pointed out that symbolic
execution in connection with assignable-clauses amounts to a relatively precise
binding time analysis (BTA). As BTA becomes rather tricky for complex lan-
guages such as
Java
, it would be interesting to use symbolic execution and our
simple partial evaluator to bootstrap a sophisticated partial evaluator for
Java
.
It could also be interesting to use symbolic execution in addition to partial eval-
uation to improve precision, for example, in the test case generation approach
of [21] discussed in the previous section.
The example in Sect. 5 shows that interleaving partial evaluation and symbolic
execution has potential for speed-up especially for programs that are written
generically. This is the case for two software development paradigms that gained
much popularity in recent times:
model-driven development
(MDD) and
soft-
ware product line
(SWPL) engineering. In both cases, development takes place
as much as possible on a generic level: in MDD programs are modelled in abstract
notations (the Platform Independent Model) and code generation is used to de-
rive Platform-Specific Models and actual code; in SWPL one separates Domain
Engineering which includes feature modeling and library development from Ap-
plication Engineering where code is derived via instantiation and composition.
