特別研究報告 概要: 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メソッドの規則を満たさ ない実装を発見することができた． タグ: Java, Formal, Verification, Satisfiability, Modulo, Theories

@mastersthesis{尾ノ上博樹2014,
  author = {尾ノ上 博樹},
  title = {JavaにおけるequalsメソッドとhashCodeメソッドの検査ツールの実装と評価},
  school = {大阪大学},
  type = {Bachelor's Thesis},
  year = {2014},
  month = {feb}
}