| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2014-03-11 11:30 JavaにおけるequalsメソッドとhashCodeメソッドの整合性の検査手法の提案 榛葉浩章・○尾ノ上博樹・岡野浩三・楠本真二（阪大）  SS2013-75 |
|
| 抄録 | （和） | 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) / / / | |
| 文献情報 | 信学技報, vol. 113, no. 489, SS2013-75, pp. 19-24, 2014年3月. | |
| 資料番号 | SS2013-75 | |
| 発行日 | 2014-03-04 (SS) | |
| ISSN | Print edition: ISSN 0913-5685 Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | SS2013-75 |
|
| 研究会情報 | |
| 研究会 | SS |
| 開催期間 | 2014-03-11 - 2014-03-12 |
| 開催地（和） | てんぷす那覇：第１・２会議室 |
| 開催地（英） | Tenbusu Naha |
| テーマ（和） | 一般 |
| テーマ（英） | Software Science |
| 講演論文情報の詳細 | |
| 申込み研究会 | SS |
| 会議コード | 2014-03-SS |
| 本文の言語 | 日本語 |
| タイトル（和） | 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) |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 榛葉 浩章 / Hiroaki Shimba / シンバ ヒロアキ |
| 第1著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 尾ノ上 博樹 / Hiroki Onoue / オノウエ ヒロキ |
| 第2著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 岡野 浩三 / Kozo Okano / オカノ コウゾウ |
| 第3著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 第4著者 氏名（和/英/ヨミ） | 楠本 真二 / Shinji Kusumoto / クスモト シンジ |
| 第4著者 所属（和/英） | 大阪大学 (略称： 阪大) Osaka University (略称： Osaka Univ.) |
| 講演者 | 第2著者 |
| 発表日時 | 2014-03-11 11:30:00 |
| 発表時間 | 30分 |
| 申込先研究会 | SS |
| 資料番号 | SS2013-75 |
| 巻番号（vol） | vol.113 |
| 号番号（no） | no.489 |
| ページ範囲 | pp.19-24 |
| ページ数 | 6 |
| 発行日 | 2014-03-04 (SS) |
[研究会発表申込システムのトップページに戻る]