概要: Javaにおいて，コレクションに格納されるオブジェクトはequalsメソッドとhashCodeメソッドをオーバーライドしている必要があり，これらのメソッドには満たすべき規則(反射性，対称性，推移性など)が存在する．この規則に違反したオブジェクトをコレクションに格納して使用した場合，正しい振る舞いをしなくなってしまい，さらにはそれによって引き起こされる欠陥を発見することが難しくなる． 既存研究では，equalsメソッドのみを対象として，満たすべき規則に違反しているかどうかを軽量的手法によって検査する手法が提案されている．この手法ではJavaコードをAlloyに変換し，Alloy Analyzerによって検査を行っている．しかし，equalsメソッドをオーバーライドするときは常にhashCodeメソッドもオーバーライドすべきであり，hashCodeメソッドの満たすべき規則はequalsメソッドに依存している．よって，hashCodeメソッドはequalsメソッドと整合性がとれていなければならず，両方のメソッドの規則違反を検査すべきである． 本研究では，Javaを対象をしてequalsメソッドとhashCodeメソッドの整合性を検査する手法を提案する．既存研究では，Alloy Analyzerを用いて軽量的な検査を行っていたが，これは内部でSATソルバを使用しており，hashCodeメソッドで行われる算術演算のモデル化には向いていない．そこで，本手法ではJavaコードをSMTソルバへの入力言語であるSMT-LIBに変換し，SMTソルバによって検査を行う．SMTソルバはSATに算術式を追加したものであり，算術演算のモデル化が行いやすく，Alloy Analyzerでは扱うことができないビット演算も扱うことができる． また，提案手法を実プロジェクトに対して適用して評価を行った．結果として実プロジェクトの中で欠陥を誘発する実装を発見することができた． タグ: checking, consistency, equals, formal, hashcode, java, methods, verification

@mastersthesis{榛葉浩章2014,
  author = {榛葉 浩章},
  title = {JavaにおけるequalsメソッドとhashCodeメソッドの整合性の検査},
  school = {大阪大学},
  year = {2014},
  month = {feb}
}