一个支持规约获取的形式规约语言

该文介绍了形式规约语言LFC设计的一些主要方面，并通过例子说明了LFC的一些特色。形式规约语言LFC是为支持软件形式规约的获取工作而开发的。该语言以一种新的递归函数，即定义在上下文无关语言上的递归函数为基础，以上下文无关语言为数据类型，在语言级支持规约获取。LFC语言已被用作形式规约获取系统SAQ的一部分。使用表明，LFC是一个能力强、易使用的语言，适合软件形式规约获取之用，并且适合其它一些用途。

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.