| 研究概要 |
入力xから出力yへの関数fを、その対応を与える一階述語論理式F(x,y)から導出するための一手法について研究を行なった。特に、∀zG(x,y,z)の形式の論理式からの導出に焦点を絞った。本手法を一階述語論理式の定理証明手法とみなすこともでき、その場合、上の論理式からの関数導出は、∀x∃y∀zG(x,y,z)という限定した形式の論理式に対する定理証明となる。本手法は、あらかじめ用意した変換規則を適用することにより、実行可能コードとしての関数fを生成する。変換規則は、論理式の変形を行なう変形規則と、関数の導出を行なう導出規則の二つに大別できる。まず導出規則を適用し、適用可能な導出規則がない場合に補助として変形規則を適用する。本研究では、まず導出手法の概要を決めた。次に、具体例として、図書館の書庫管理システムの仕様に本手法を適用して、その詳細について評価を行なった。最後に、導出の停止性および正当性について検証して、本手法の有効性の評価を行なった。
|
