Formal V erification Technique for Consistency Checking between equals and hashCode Methods in Java
Hiroaki Shimba, Onoue Hiroki, Kozo Okano, Shinji Kusumoto · IEICE Technical Report; IEICE Tech. Rep. · 2014
Java objects used with the standard collection should override both of its equals and hashCode methods. Both methods need to satisfy the consistency rules or unex- pected behaviors may cause faults that are hard to detect. A previous study checked whether an equals method satisfies part of the consistency rule. To avoid unexpected behaviors, however, it is necessary to check that both the equals and the hashCode methods satisfy the rules. This research proposes a method which checks the consistency between equals and hashCode methods in Java. We model Java source code and check whether both methods satisfy the rules using an SMT solver called Z3. We applied our proposed method to some practical projects. As results, we detected some Java source code that violates the rules.