The Research Of Algorithm Specification Based On Structured Natural Language

Formal method is a pivotal technology to copy with software crisis and to implement software automation. Andmore, algorithm designing is the soul of software designing. Through researching deeply on algorithmic program, professor Xun Jinyun present a formal method named PAR(the abbreviation of partition-and-recur) method, it bases on the relation of partition and recurrence. When we implement software by using formal methods, we must define the precise program specification of the software. However, in order to avoid different meanings of natural language, nowadays, formal methods descript specification with methmatics methods. Ones who use them to descript specification must master mathmatics theory of relational domain, And so it confines to popularize the formal methods. These motivate the research of this dissertation.This dissertation investigates deeply on the relation between natural language and algorithm specification and presents a structured natural language (SNL language) to descript algorithm specification, and gets the following results:1. In order to slove the definition problem of algorithm specification, this dissertation proposes SNL Language which is based on natural language, elementary mathsmatic formula, simple quantifier and abstract data type, defines the grammer of SNL language. Defining algorithm specification by SNL language, it is not necessary to master advanced mathmatics theory but SNL language.2. In order to solve multiformity of express method by natural language, in this dissertation we collect a mass of words about SNL language and specification, create a multilingual word corpus.3. Sometimes the affirmation in algorithm specification is so complicated that it is very difficult to be descripted by a predication formula. In order to slove this problem, the dissertation proposes using and-sub-predication formulae to descript specification in SNL language. This express method is close to human being's thinking mode, and it is simple.4. In this dissertation, we define an algorithm corpus to collect algorithms those had been designed, and then we can use these algorithms to define new and complicated program specification.5. By using OOA and OOD technology and Java programming language, we implement SNL Language Algorithm specification to RADL Specification Conversion System.