权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

基于谓词逻辑的规范从可执行代码派生系统的原型评估

基本信息

批准号：
06680330
负责人：
深澤良彰
金额：
$ 0.9万
依托单位：
Waseda University
依托单位国家：
日本
项目类别：
Grant-in-Aid for General Scientific Research (C)
财政年份：
1994
资助国家：
日本
起止时间：
1994 至无数据
项目状态：
已结题

项目摘要

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

A study of the application and requirements of the first-order logic and the functional forms of the system. The purpose of this study is to derive and support the implementation of a first-order statement logic expression. This study is based on the analysis of the number of possible problems. This study proposes two kinds of transformation rules for logical expressions and related numbers. The logical connection between the number of symbols and the number of elements of the theoretical formula is the same as that of the transformation rule. The results of this study demonstrate that the rules of derivation are applicable, applicable, and applicable. The results of this study are derived from the following three parts: the first part is the standardization of logical expressions, the second part is the application of transformation rules, and the third part is the composition of transformation rules. In particular, any first-order predicate logic expression is impossible to change mechanically, and it is necessary to restrict the predicate logic expression. This study is to determine whether the problem is solved by using the above method.