Tweet | |
尾ノ上, "JavaにおけるequalsメソッドとhashCodeメソッドの検査ツールの実装と評価," , 2014年2月. | |
ID | 336 |
分類 | 学位論文 |
タグ | Java Formal Verification Satisfiability Modulo Theories |
表題 (title) |
JavaにおけるequalsメソッドとhashCodeメソッドの検査ツールの実装と評価 |
表題 (英文) |
Implementation and Evaluation of Inspection Approach for Equals and Hashcode Method in Java |
著者名 (author) |
尾ノ上 博樹 |
英文著者名 (author) |
Hiroki Onoue |
キー (key) |
Hiroki Onoue |
刊行月 (month) |
2 |
出版年 (year) |
2014 |
刊行形式 (howpublished) |
|
URL |
|
付加情報 (note) |
特別研究報告 |
注釈 (annote) |
|
内容梗概 (abstract) |
JavaにおいてequalsメソッドとhashCodeメソッドはObjectクラスで
定義されており,コレクションフレームワークに格納されるような データ構造を表すクラスにおいて重要である.原則として,equals メソッドをオーバーライドする場合はhashCodeメソッドもオーバー ライドしなければならない.これらのメソッドには満たすべき規則 が存在し,その規則を満たさない実装を行った場合,本来それらの メソッドに期待されている振舞いが保証されなくなる.さらには, 想定外の振舞いによって発見の難しい欠陥を誘発する可能性がある . 既存研究では,equalsメソッドのみを対象として満たすべき規則を 満たしているかを軽量形式手法によって検査する手法が提案されて いる.この手法ではJavaコードをAlloyを用いてモデル化しAlloy Analyzerによって検査を行っている.しかし,一般にequalsメソッ ドがオーバーライドされている場合はhashCodeメソッドも同時にオ ーバーライドされているため,両方のメソッドを検査すべきである . 著者の属する研究グループではequalsメソッドだけでなくhashCode メソッドも対象とした検査手法が提案されている.この手法では hashCodeメソッドを検査するためにAlloyではなくSMT-LIBを用いて モデル化を行い,SMTソルバの1つであるZ3によって検査を行う. 本研究ではこの手法の一部をEclipseプラグインとして実装し,い くつかのオープンソースプロジェクトに対して適用し評価を行った .結果として,equalsメソッドやhashCodeメソッドの規則を満たさ ない実装を発見することができた. |
論文電子ファイル | graduation-thesis.pdf (application/pdf) [一般閲覧可] |
BiBTeXエントリ |
@misc{id336, title = {JavaにおけるequalsメソッドとhashCodeメソッドの検査ツールの実装と評価}, author = {尾ノ上 博樹}, month = {2}, year = {2014}, note = {特別研究報告}, } |