B-010
形式仕様記述の細分化における未記述制約抽出手法の提案

◎森下匡平・織田　健（電通大）

B methodは集合論に基づいた記述と段階的詳細化を用いて仕様記述からコード生成までの過程を支援する形式手法である。我々は、仕様記述を細分化し同等の操作を行う既存のソフトウェア部品を検索・自動合成することで新しいソフトウェアを生成する手法を提案している。細分化前の仕様記述が持つ制約を維持し、細分化後の仕様記述の無矛盾性を保持する事が必要不可欠であるが、未記述制約の抽出が不十分である。　本研究では、仕様内に暗黙的に存在する制約を推論により抽出する事で仕様の細分化における無矛盾性の保持を図る。そのため、記述されている制約から未記述の制約を推論する手法と推論による制約数爆発を防ぐ手法を提案する。