| 講演名 | 2014-03-11 JavaにおけるequalsメソッドとhashCodeメソッドの整合性の検査手法の提案 榛葉 浩章, 尾ノ上 博樹, 岡野 浩三, 楠本 真二, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | Javaにおいて,コレクションに格納されるオブジェクトはequalsメソッドとhashCodeメソッドをオーバーライドしている必要があり,これらのメソッドには満たすべき規則が存在する.この規則に違反したオブジェクトをコレクションに格納して使用した場合,正しい振る舞いをしなくなってしまい,さらにはそれによって引き起こされる欠陥を発見することが難しくなる.既存研究ではequalsメソッドのみを対象として満たすべき規則に違反しているかどうかを軽量形式手法で検査する手法が提案されている.しかし, equalsメソッドをオーバーライドするときは常にhashCodeメソッドもオーバーライドすべきであり,両方のメソッドの規則違反を検査すべきである.本研究ではJavaを対象としてequalsメソッドとhashCodeメソッドの整合性を検査する手法を提案する.本手法ではJavaソースコードをモデル化し,SMTソルバZ3によって検査を行う.また,提案手法を実プロジェクトに適用し,実プロジェクトの中で規則に違反しているコードを発見することができた. |
| 抄録(英) | 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. |
| キーワード(和) | Java / equalsメソッド / hashCodeメソッド / 形式的検証 / Satisfiability Modulo Theories(SMT) |
| キーワード(英) | Java / equals method / hashCode method / Formal Verification / Satisfiability Modulo Theories(SMT) |
| 資料番号 | SS2013-75 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2014/3/4(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | JavaにおけるequalsメソッドとhashCodeメソッドの整合性の検査手法の提案 |
| サブタイトル（和） | |
| タイトル（英） | Formal Verification Technique for Consistency Checking between equals and hashCode methods in Java |
| サブタイトル（和） | |
| キーワード(1)（和/英） | Java / Java |
| キーワード(2)（和/英） | equalsメソッド / equals method |
| キーワード(3)（和/英） | hashCodeメソッド / hashCode method |
| キーワード(4)（和/英） | 形式的検証 / Formal Verification |
| キーワード(5)（和/英） | Satisfiability Modulo Theories(SMT) / Satisfiability Modulo Theories(SMT) |
| 第 1 著者 氏名（和/英） | 榛葉 浩章 / Hiroaki SHIMBA |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 尾ノ上 博樹 / Hiroki ONOUE |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 岡野 浩三 / Kozo OKANO |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 4 著者 氏名（和/英） | 楠本 真二 / Shinji KUSUMOTO |
| 第 4 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2014-03-11 |
| 資料番号 | SS2013-75 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | 489 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |