◎三鍋孝介・織田　健（電通大）

ソフトウェア部品の検索において要求を満たす部品の検索は困難である。形式手法 B Method は、数学的に書かれた仕様（モデル）と実装の整合性を保証できる。そのため部品を B Method で構築すると、定理証明を用いて数学的に等価なモデルの検索が可能である。我々は既存の B Method のソフトウェアを分割してこのような部品を整備する方法を提案している。検索時の数学的等価性判定の計算コストを下げるため文字列一致による検索を目指し、事前推論による等価なモデルの字面統一を図る。本発表ではソフトウェアを分割して字面の統一されたモデルを持つ部品を得るアルゴリズムを提案する。