RT Journal Article
JF 2010 17th Working Conference on Reverse Engineering
YR 2010
VO 00
SP 205
TI An Abstraction-Oriented, Path-Based Approach for Analyzing Object Equality in Java
A1 Chandan R. Rupakheti,
A1 Daqing Hou,
K1 model checking
K1 path-based program analysis
K1 equality
K1 abstraction recognition
AB The standard collection data structures in Object-Oriented languages require their element classes provide a predicate to compare two objects for equality. Among other correctness requirements, this predicate must be an equivalence relation. The chance of mistakes increases when equality is implemented in a type hierarchy. Detection of such problems requires reasoning about the equality at a higher level semantics than the code, involving the state, the behavior, and the sub-typing relations in the type hierarchy. We present a path-based, abstraction-oriented approach to checking the correctness of equality implementation in a type hierarchy. In our approach, code patterns on paths are identified and translated into abstractions in Alloy. The Alloy model is then automatically checked to reveal any problems related to the equivalence relation. Our evaluation shows that this approach (1) found problems in the production code, and (2) scaled to a project as large as JDK 1.5. We believe that it has a potential to be used on a developer's desktop on a daily basis.
PB IEEE Computer Society, [URL:http://www.computer.org]
SN 1095-1350
LA English
DO 10.1109/WCRE.2010.30
LK http://doi.ieeecomputersociety.org/10.1109/WCRE.2010.30