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

A Formal Specification Language Supporting Specification Acquisition

作　　者：陈海明[1] 董韫美[1] 

机构地区：[1]中国科学院软件研究所计算机科学重点实验室,北京100080

出　　处：《计算机学报》2002年第5期459-466,共8页Chinese Journal of Computers

基　　金：国家自然科学基金 (69873 0 42 ;60 10 3 0 0 8);国家"九五"科技攻关计划(98-780 -0 1-0 7-0 2 )资助

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

关 键 词：规约获取 形式规约语言 上下文无关语言 递归函数 计算机 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]