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

形式手法の1つとして、数学的な仕様記述からコード生成までを支援するB-Methodがある。
B-Methodの仕様と実装を細分化しソフトウェア部品として整備することで、再利用性を高めることができ、高信頼な新規ソフトウェアを低コストで作成することが可能となる。
本研究では、仕様と実装間の制約条件により変数の対応関係を特定することで、細分化された仕様を満たす実装の部品の機械的な抽出を目指す。しかし仕様と実装間でデータ構造が異なっていたり、写像を用いた操作が存在したりする場合、仕様と実装間の変数の対応が単純ではないことがあるため、本稿ではこれらの問題を解消した実装抽出手法を提案する。