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.