| Presentation | 2014-03-11 Formal Verification Technique for Consistency Checking between equals and hashCode methods in Java Hiroaki SHIMBA, Hiroki ONOUE, Kozo OKANO, Shinji KUSUMOTO, |
|---|---|
| PDF Download Page |  PDF download Page Link |
| Abstract(in Japanese) | (See Japanese page) |
| Abstract(in English) | Java classes must observe constraints on "hashCode" methods as well as "equals" methods, in order to behave correctly when their objects are interacted with the Java collection frameworks. One of researches on the consistency of such methods has proposed a lightweight formal method. This approach checks whether a given "equals" method observes the rules such as reflexivity, symmetry, and transitivity using Alloy Analyzer, a model finder. In general a class overridden with "equals" method must override its "hashCode" method properly. Therefore, we present a formal verification technique for consistency checking between "equals" and "hashCode" methods in Java. We translate Java code to SMT-LIB and verify it by Z3. Furthermore, our approach has been evaluated on open source projects. As a result of evaluation, we detected some violations in the projects. |
| Keyword(in Japanese) | (See Japanese page) |
| Keyword(in English) | Java / equals method / hashCode method / Formal Verification / Satisfiability Modulo Theories(SMT) |
| Paper # | SS2013-75 |
| Date of Issue |
| Conference Information | |
| Committee | SS |
|---|---|
| Conference Date | 2014/3/4(1days) |
| Place (in Japanese) | (See Japanese page) |
| Place (in English) | |
| Topics (in Japanese) | (See Japanese page) |
| Topics (in English) | |
| Chair | |
| Vice Chair | |
| Secretary | |
| Assistant | |
| Paper Information | |
| Registration To | Software Science (SS) |
|---|---|
| Language | JPN |
| Title (in Japanese) | (See Japanese page) |
| Sub Title (in Japanese) | (See Japanese page) |
| Title (in English) | Formal Verification Technique for Consistency Checking between equals and hashCode methods in Java |
| Sub Title (in English) | |
| Keyword(1) | Java |
| Keyword(2) | equals method |
| Keyword(3) | hashCode method |
| Keyword(4) | Formal Verification |
| Keyword(5) | Satisfiability Modulo Theories(SMT) |
| 1st Author's Name | Hiroaki SHIMBA |
| 1st Author's Affiliation | Graduate School of Information Science and Technology, Osaka University() |
| 2nd Author's Name | Hiroki ONOUE |
| 2nd Author's Affiliation | Graduate School of Information Science and Technology, Osaka University |
| 3rd Author's Name | Kozo OKANO |
| 3rd Author's Affiliation | Graduate School of Information Science and Technology, Osaka University |
| 4th Author's Name | Shinji KUSUMOTO |
| 4th Author's Affiliation | Graduate School of Information Science and Technology, Osaka University |
| Date | 2014-03-11 |
| Paper # | SS2013-75 |
| Volume (vol) | vol.113 |
| Number (no) | 489 |
| Page | pp.pp.- |
| #Pages | 6 |
| Date of Issue | |