尾ノ上, "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 = {特別研究報告},
}