| Project/Area Number |
06680330
|
|---|
| Research Category |
Grant-in-Aid for General Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
深澤 良彰 早稲田大学, 理工学部, 教授 (20165252)
|
|---|
| Project Period (FY) |
1994
|
| Project Status |
Completed (Fiscal Year 1994)
|
| Budget Amount *help |
¥1,400,000 (Direct Cost: ¥1,400,000)
Fiscal Year 1994: ¥1,400,000 (Direct Cost: ¥1,400,000)
|
|---|
| Keywords | 仕様記述言語 / 形式的仕様 / 述語論理 / プロトタイプ / プロトタイピング / 直接実行 |
|---|
| Research Abstract |
一階の述語論理を用いて、要求するソフトウェアの機能を形式的に定義し、それに基づく開発過程を提唱する研究がある。本研究の目的は、一階の述語論理式から実行可能なコードを導出し、その実行によつて仕様の検証を支援することであった。
本研究では、実行可能コードを関数に定めている。これを得るためには、本研究で提唱した導出手法では、述語論理式の変形規則と関数の導出規則の2種類の変換規則と作成した。論理接続や限量記号や組込み述語などの理論式の構成要素に対して、変換規則を複数回適用することにより、関数を得ることができることがわかった。この際には、通常は、まず、導出規則を適用し、適用可能な導出規則がない場合の補助として、変形規則を適用することが有効なことも、本研究の結果判明した。
これらの成果を得るための導出システムは、変換規則のライブラリ、論理式の標準化を行う部分、メタ規則に基づいて変換規則を適用する部分の3つのパトから構成した。特に、任意の一階述語論理式からの実行可能コードの機械的な変換は不可能であるので、対象の述語論理式を制限する必要があることが大きな問題点となっていた。本研究で課した制約は、実用上ほとんど問題がないことも判明した。
|
