首页 >> 收录期刊 >> 计算机学报 >> 正文
杂志中文名:计算机学报
杂志英文名:Chinese Journal of Computers
主管单位:中国科学院 中国科协
主办单位:中国计算机学会 中国科学院计算技术研究所
地址:中国科学院计算技术研究所(北京2704信箱)
邮编:100190
电话:010-62620695;
Email:cjc@ict.ac.cn
ISSN:0254-4164
主编:高文












一个支持规约获取的形式规约语言
引用本文:陈海明,董韫美.一个支持规约获取的形式规约语言[J].计算机学报,2002,25(5):459-466.
作者姓名:陈海明  董韫美
作者单位:中国科学院软件研究所计算机科学重点实验室,北京,100080
基金项目:国家自然科学基金 (69873 0 42 ,60 10 3 0 0 8),国家“九五”科技攻关计划(98-780 -0 1-0 7-0 2 )资助
摘    要:该文介绍了形式规约语言LFC设计的一些主要方面,并通过例子说明了LFC的一些特色。形式规约语言LFC是为支持软件形式规约的获取工作而开发的。该语言以一种新的递归函数,即定义在上下文无关语言上的递归函数为基础,以上下文无关语言为数据类型,在语言级支持规约获取。LFC语言已被用作形式规约获取系统SAQ的一部分。使用表明,LFC是一个能力强、易使用的语言,适合软件形式规约获取之用,并且适合其它一些用途。

关 键 词:规约获取  形式规约语言  上下文无关语言  递归函数  计算机
修稿时间:2001年4月28日
作者简介:陈海明,男,1966年生,博士,副研究员,目前主要研究方向是软件设计方法.E-mail: chm@ios.ac.cn.董韫美,男,1936年生,研究员,中国科学院院士,目前主要研究方向是软件设计方法.

A Formal Specification Language Supporting Specification Acquisition
CHEN Hai,Ming,DONG Yun,Mei.A Formal Specification Language Supporting Specification Acquisition[J].Chinese Journal of Computers,2002,25(5):459-466.
Authors:CHEN Hai  Ming  DONG Yun  Mei
Abstract: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.
Keywords:formal specification language  context  free language  recursive function  
本文献已被 CNKI 维普 万方数据 等数据库收录!