B-003
リファインメントを考慮した形式的ソフトウェア合成アルゴリズム

◎叶野英俊・織田　健（電通大）

形式手法の1つとして仕様記述からコード生成までを支援するB Methodがあり、これは数学的な仕様とその詳細である実装、及びそれらの中間的記述であるリファインメントからなる。我々は、これらを分解し再利用することで高信頼ソフトウェアを低コストで生成する手法を提案しているが、リファインメントを考慮した手法は抽象的な提案に留まっている。
そこで本研究では、この抽象的な手法を詳細化したアルゴリズムを提案する。このときリファインメントの段数や変数の詳細化順序の不一致などの問題が存在するため、変数の関係を示すリンク不変条件や変数の型を利用することでこれらの問題を解決する。