The Community for Technology Leaders
2013 20th Working Conference on Reverse Engineering (WCRE) (2010)
Beverly, Massachusetts USA
Oct. 13, 2010 to Oct. 16, 2010
ISSN: 1095-1350
ISBN: 978-0-7695-4123-5
pp: 205-214
ABSTRACT
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.
INDEX TERMS
model checking, path-based program analysis, equality, abstraction recognition
CITATION
Chandan R. Rupakheti, Daqing Hou, "An Abstraction-Oriented, Path-Based Approach for Analyzing Object Equality in Java", 2013 20th Working Conference on Reverse Engineering (WCRE), vol. 00, no. , pp. 205-214, 2010, doi:10.1109/WCRE.2010.30
99 ms
(Ver 3.3 (11022016))