論理型形式的仕様のプロトタイピング・システムの試作・評価

1995 Fiscal Year Annual Research Report

• Project/Area Number: 07680373
• Research Category: Grant-in-Aid for General Scientific Research (C)
• Research Institution: Waseda University
• Principal Investigator: 深澤 良彰 早稲田大学, 理工学部, 教授 (20165252)
• Keywords: 形式的仕様 / プロトタイプ / 述語論理 / 導出規則 / プログラム合成

Research Abstract

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

Research Products

• [Publications] 小野康一,河野誠一,深澤良彰: "述語論理に基づく仕様からの実行可能コードの導出技法" 早稲田大学情報科学研究教育センター紀要. 18. 18-26 (1996)
• [Publications] 小野康一,深澤良彰: "実行時仕様記述言語ZXの導入による高レベル形式的仕様の実行" レクチャーノート/ソフトウェア学. 15. 121-130 (1996)