A Formal Specification Language Supporting Specification Acquisition

Although formal specification techniques are very useful in software development, specification acquisition is a difficult task. The task is further complicated by the fact that none of the known formal specification languages is designed to support specification acquisition at language level. Equally important is the validation of the acquired specifications, which is the process to confirm that the specifications meet the user's true requirements.This paper presents the formal specification language LFC which is designed to support formal specification acquisition and validation of software. In order to achieve the goal, two powerful formalisms, i.e. formal languages and recursive functions, are employed in LFC. The language is based on a new kind of recursive functions, i.e. recursive functions defined on context free languages(CFRF), and uses context free language as data type. These enable the use of machine learning and other machine aided techniques in specification process to reduce acquisition difficulty, while possessing strong expressiveness for representing specifications. As a result LFC supports specification acquisition at language level. The language is also executable; therefore it enables rapid prototyping. Specifications acquired are validated by prototyping and other techniques. The major novelty in the design of LFC is the utilization of formal languages and CFRF, a new and useful tool for specifying non numeric algorithms, as the theoretical basis of the language. The main aspects of the design of language LFC are introduced, including theoretical preparations, and major features of the language. A few small examples are presented to illustrate some features of the language. Implementation of LFC is also briefly reviewed.The language has been used as a constituent part of the formal specification acquisition system SAQ. Some nontrivial experiments have been conducted. The results show that LFC is powerful and easy to use, suitable for specification acquisition, as well as for some other purposes. Some problems are discussed and future directions are suggested.