【面向对像规格说明语言及转换的研究】陈伟.pdf

本文提出了一种面向对象规格说明语言一J0OPDL语言,它以一阶谓词逻辑的描述方法对概要设计进行规格说明,其中,规格型部件是概要设计的基本单位,也是可重用的基本单位.本义还探讨了基于这种语言从概要设计到详细设计的自动/半自动转换问题,这种转换的关键是规格型部件到实现型部件的转换,为此、我们提出了已知量、未知度、层次、延迟处理等概念和相应的解决方法。

第一章前言随有计机科学的不断发展,以及软件技术的不断提高,软件的形式化刀发和软付设订的白动化越来越受到人们的关注,这也是计算近儿十年来,计算机硬件能力有了很大提高,而软件的生产相对发展较慢,难以满足人们的要求,出现了所谓的“软件危机”,软件开发成为计竹机使用中的瓶颈部分,软件自动化是解决这种矛盾,提高软件产率的根本途径,面且自动化可以使软件的可靠性,易维护软件自动化是指,尽可能借助系统完成软件开发,在不同程度上从软件功能规格说明到可执行程序代码的自动生成,软件功能规格说明是高层次的规范,是一种粗略的功能描述,它只是对最初人们希望解决的间题的描述:而最后的目标代码是低层次的,

以用面向对象的方法对软件系统的设计进行描述,它以代数语义作为在COLD-K中,用类的概念休现血向对象的设计息想.这里,类可以看做是包含-个状态集和一个初始状态的抽象机,在对类的状态的描述中用到三种状态成分(statcconponents):种名(sort names)调词名和函数名.而日类的状态可以用过程的方法来改变,即过程通过谓词或的数的修改来改变状态,函数或诏词的修改就是指修 COLD-K语言中没有传统意义1变量的概念,它们都用谓词、函数和过程来表示,对函数、谓词和过程的语义描述,采用了公理和归纳说明的方法,公理方法是指对类中某个成分属性(property)的断言(assc