Information Technology Reference
In-Depth Information
In this paper, we propose a new approach to handle the precondition in a DSE tool,
written in the tested language. It is based on a late exploration of the precondition's
code during the test generation. This paper also provides an experimental evaluation of
the late-precondition technique implemented in P
AT H
C
RAWLER
. Our approach offers
a greater expressiveness than P
AT H
C
RAWLER
's native precondition. Our experiments
also show that the late-precondition approach offers comparable performances to the
native precondition and better performances than another alternative approach.
The paper is organized as follows. First, Sec. 2 gives a brief overview of precondition
handling. Next, Sec. 3 describes the new method, while Sec. 4 evaluates it experimen-
tally. Finally, Sec. 5 concludes the paper.
2
Related Work
Some test input generation tools allow to express the precondition in the tested lan-
guage. Tools like Korat [2] are specifically designed to generate valid inputs based on
such a precondition without considering the code of the program under test. However,
a few code-based test generation tools may also handle the precondition that way. For
instance, Java PathFinder [3] (generalized symbolic execution) and CUTE [4] (DSE)
allow the user to provide a consistency check as a function in the tested language. The
function is first solved, using the normal process of the tool. Similarly, Pex [5], a DSE
tool for the .NET platform, treats Code Contracts, an embedded form of specification
that is automatically translated into dynamic checks during compilation. For the pre-
condition, assumption statements are placed
before
the code to be tested and handled
as any other part of the code. Many DSE tools do not address the precondition problem
specifically. However, at the cost of extra test cases, the precondition can be written as a
conditional statement around the program code, leading to a solution almost equivalent
to previous approaches. Like these tools, our approach proposes to encode the precon-
dition in the tested language. However, it separates and delays the exploration of the
precondition in order to minimize the exploration of the program code. To the best of
our knowledge, this approach has never been used in other tools.
Another way to enforce the precondition is to describe how to construct a valid input
rather than how to check whether a test case is valid. This method, sometimes called
finitization
[2], is dual to a classic precondition. Indeed, some complex structures are
simpler to check than to construct, while others are better handled constructively.
The late-precondition method combines multiple symbolic executions. A related
combination of symbolic executions is
compositional symbolic execution
proposed by
Godefroid [6]. It aims at separating the symbolic execution of called functions in order
to maximize reuse and to limit path exploration by generating so-called
function sum-
maries
. Our late-precondition method has another objective. Indeed, it only separates
the symbolic execution of two components (program and precondition) and does not
create summaries. However, our late-precondition has a remarkable trait: the precondi-
tion is considered after the program. This ensures that the program's paths are explored
only once without requiring to compute and store function summaries.
