Information Technology Reference
In-Depth Information
recursively built from subexpressions. It then traverses this AST and translates it to Java
in the following manner: Minshar views Java objects as one-element sets and navigates
the data structure fields (obtained via reflection) to construct the sets that correspond
to subexpressions used in the AST, such as subexpressions that have reflective closure.
Once the sets are generated, Minshar asserts the Alloy checks and returns false if they
do not hold.
4.2
DREAM with Juzi Back-End
Juzi [8, 9] is an automated data structure repair framework. Given a corrupt data struc-
ture, as well as a repOK method that describes the invariants of the data structure, Juzi
monitors the execution of repOK which checks the invariants. Upon a failure, Juzi sys-
tematically mutates the fields of the corrupt data structure, starting from the ones that
were accessed last in repOK and trying different values, to make them satisfy the given
specifications. In addition to repairing the data structure, Juzi reports the mutations it
performed in a log file that holds a sequence of tuples
<O
1
,f,O
2
>
, i.e., an assign-
ment to field
f
of object
O
1
to the value
O
2
- each tuple represents a repair action.
Juzi has two properties that make it a good fit for DREAM. First, it uses checks
written in Java (i.e., repOK methods) instead of Alloy or other specification languages.
Second, once it reports a faulty data structure, it also reports the field that is responsible
for the failure of the repOK method on the current data structure. DREAM uses these
properties of Juzi to facilitate finding effective repair abstractions. The first property
provides a fast way of checking the correctness without a need to translate specifications
to Java (as it was the case with Alloy for which we used Minshar). The second property
pinpoints to the exact object and field that need mutation in the current faulty data
structure, taking care of the left hand side and the filed of the repair action.
As with any other repair framework, every time Juzi finds a correct fix for a specifi-
cation violation, DREAM computes an abstraction for the repair. For example, if Juzi
repairs the data structure by assigning a field
f
of an object
O
to
null
,thenDREAM
records
O.f = null
, meaning that if
f
needs to be mutated, it should be set to
null
.
Thereby, DREAM prioritizes
null
when a future execution encounters the same error
even if the underlying repair routine would have first tried a non-null value according
to its default search.
Juzi has one drawback compared to Alloy based repair routines: It does not support
pre- and post-conditions of methods, only invariants. Therefore, it fails to find cases
that a method is not conforming to its specification in changing a data structure.
5
Evaluation
We present the experimental evaluation of DREAM combined with Cobbler [23] in
Section 5.1, and combined with Juzi [8, 9] in Section 5.2. All the experiments used
a 2.50GHz Core 2 Duo processor with 4.00GB RAM running 64 bit Windows 7 and
Sun's Java SDK 1.7.0 JVM. Cobbler used MiniSat and MiniSatProver SAT solvers.
