程序规范自动检测与修正系统ADRS的研究

RESEARCH ON THE ADRS SYSTEM FOR AUTOMATIC DETECTION AND REVISION OF PROGRAM SPECIFICATION

文中介绍了一个程序规范自动检测与修正系统ＡＤＲＳ的理论模型．在开放逻辑的思想基础上，文中提出了一种自动修正模型，并试图对李未提出的３个问题给出解决方案．作为对第１个问题的解决，作者提出了一种刻画程序规范重要性程度的全序结构，克服了加标记的二分法的粗糙性．作为对第２个问题的解决，作者提出了修正函数的定义和Ｒ－计算模型，并证明了该模型满足修正函数的要求．作为对第３个问题的解决，作者提出了Ｔ－修正函数的定义和ＲＴ－计算模型，证明了随修正时间的增长，Ｔ－修正函数逼近修正函数，且Ｔ－修正函数是可计算的．文中还提出了一种改进的调解方法，其中禁止等词之间的调解．该方法被用于自动检测部分的实现，使系统检测出矛盾的效率有所提高．文中证明了该方法的可靠性与完备性．

In this paper, we introduce a theoretic model of ADRS system that is used for automatic detection and revision of program specifications. Inspired by the thought of open logic, we present a model of automatic revision and try to give solutions of three problems presented by Li Wei. To solve the first problem, we present a kind of order structure for describing the importance of program specification, which avoids the roughness of dichotomy. To solve the second problem, we present the definition of revision function and R-computation model, and prove that R-computation model satisfies the property of revision function. To solve the third problem, we present the definition of T-revision function and RT-computation model, prove that T-revision function converges to revision function with the increase of revision time and Trevision function is computable. In this paper, we also present an improved paramodulation method that prohibits the paramodulation between equalities. This method is applied in the automatic detection module of ADRS system and enhances the efficiency of detection. The soundness and completeness of this paramodulation method is also proved.