A method for translating natural language program specifications into algebraic specifications
Hiroyuki Seki, Tadao Kasami, Eiji Nabika, Takashi Matsumura · Systems and Computers in Japan · 1992
Abstract A method for translating program specifications in a natural language into algebraic specifications is presented. The translation rules consist of: (a) syntax rules of the natural language; (b) rules for constructing an intermediate structure similar to “categories” in HPSG; and (c) rules for generating axioms to translate intermediate structures into axioms of the form of logical formula = =True. Based on the concept of type, which is defined by using the derivations of expressions representing the meanings of natural language sentences in a generative grammar, and based on the characteristics of the functions representing the meanings of words, a more rigorous method of solving the problems of elimination of syntax ambiguities anaphoric bindings, and sorts and scopes of quantifiers is proposed. Especially, by introducing attributes having the type information of the functions denoted by natural language phrases in the intermediate structures, ambiguities at the time of the parsing can be reduced. Also, the meaning of phrases such as verb phrases can be rigorously defined by using functions having arguments of different types for singular and plural objects. Arguments which are not explicitly specified in natural language sentences can be represented formally by introducing arguments which have types representing the states of the program. Furthermore, a method is proposed to rigorously deduce the sorts and scopes of the quantifiers by using the dependency relation between the arguments representing the meanings of the words. The results of translating the main part of the OSI session protocol are presented.