述語論理に基づく仕様からの実行可能コード導出システムの試作評価

点击翻译按钮获取中文摘要

一階の述語論理を用いて、要求するソフトウェアの機能を形式的に定義し、それに基づく開発過程を提唱する研究がある。本研究の目的は、一階の述語論理式から実行可能なコードを導出し、その実行によつて仕様の検証を支援することであった。本研究では、実行可能コードを関数に定めている。これを得るためには、本研究で提唱した導出手法では、述語論理式の変形規則と関数の導出規則の2種類の変換規則と作成した。論理接続や限量記号や組込み述語などの理論式の構成要素に対して、変換規則を複数回適用することにより、関数を得ることができることがわかった。この際には、通常は、まず、導出規則を適用し、適用可能な導出規則がない場合の補助として、変形規則を適用することが有効なことも、本研究の結果判明した。これらの成果を得るための導出システムは、変換規則のライブラリ、論理式の標準化を行う部分、メタ規則に基づいて変換規則を適用する部分の3つのパトから構成した。特に、任意の一階述語論理式からの実行可能コードの機械的な変換は不可能であるので、対象の述語論理式を制限する必要があることが大きな問題点となっていた。本研究で課した制約は、実用上ほとんど問題がないことも判明した。