情報処理学会 第75回全国大会講演要旨

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