情報処理学会第85回全国大会 会期:2023年3月2日~4日 会場:電気通信大学

4L-06
演算の可換性と結合性に配慮した形式仕様の式表現の統一のための型付き項書換えアルゴリズム
○檜垣 廉,織田 健(電通大)
我々は、形式手法B Methodの信頼性保証の枠組みを利用した、部品の再利用による高信頼ソフトウェア合成手法の研究をしている。
本手法では、要求を満たす部品を文字列一致で検索するため、項書換えにより等価な仕様を文字列上で一致させる。
従来手法では、式の型によって適用する項書換え規則を切り替えることや、可換性・結合性を持つ演算の被演算子を多重集合として扱い式の構造を統一することを提案したが、具体的なアルゴリズムを示していなかった。
本研究では、式の型や可換性・結合性を持つ演算を扱えるよう項書換え系の適用アルゴリズムを拡張し、Standard MLで実装した。(278文字)