講演抄録/キーワード |
講演名 |
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 |