Abstract:SAQ is an experimental system to perform acquisition, verification and reusing of formal specification, in which the lexical and syntactic definitions of one concept should be integrated into one context-free grammar. If employed conventional context-free grammars to describe the overall definitions of complicated concepts such as natural languages and programming languages, separators such as spaces and carrier returns should be included and the definitions should be very messy. To solve this problem, a special kind of context-free grammars is presented. The grammars are obtained by dividing the set of non-terminals and the set of terminals of conventional context-free grammars into two respectively. As a result, the grammatical definitions of complicated concepts are relatively neat; at the same time, lexical analysis and syntax analysis can be integrated into one parsing process. In addition, the authors present the corresponding parsing and derivation tree construction algorithms, which are obtained on the basis of the general parsing method of Earley and its corresponding algorithm of construction of rightmost derivation respectively.