基于前后断言的多线程形式功能规格说明语言

探索用基于公理语义的前后断言方法来刻划多线程程序的功能，设计了一个功能规格说明语言ＪＡＶＡＳＰＥＣ，用来形式地表达程序的功能规格说明，为支持多线程的Ｊａｖａ程序自动生成奠定了基础     

基于C++STL的Z规格说明数据类型的表示

介绍了Z规格说明的数据类型和它们的分类,从定义出发,阐述了这些数据类型派生的派生与继承关系．以Z规格说明向可执行代码的自动转换为目的,结合C 语言中STL模板库对数据结构和通用算法的强大支持功能,提出了用STL中的容器表示Z规格说明数据类型的方法。     

基于逻辑系统的用户需求功能规格说明语言及其应用

在基于谓词逻辑对知识的表示的基础上，用Unity逻辑系统对其加以扩充，形成一个小型的用户需求功能规格说明语言（Small problem Specification Language），用这种形式化的语言对电梯控制系统作出形式化的用户需求功能规格说明。     

Object-Z规格说明的结构模拟动画技术

形式化方法让软件需求的规格说明变得更加简洁精确,但是它的抽象难懂让用户难以确定形式规格说明中所叙述的用户需求就是他们所期望的.另外,大多的规格说明语言都是不可执行的,因此人们采用一种动画模拟的方式,将形式规格说明转换成一种可模拟执行的形式,从而帮助用户和规格说明者确认形式规格说明是否与用户的非形式化需求相一致.通过分析比较形式规格说明的两种动画策略———形式化程序合成和结构模拟的优缺点,决定使用结构模拟技术将Object-Z规格说明转换成SICStus Prolog可执行程序并加以执行,从而实现对Object-Z规格说明的确认.     

一个Z的证明责任产生器

在写出规格说明后,需要对规格说明的严密性进行证明,定理证明则可以消除规格说明中的模糊性和不一致性,从而验证规格说明是否满足用户需求．证明责任是从规格说明中产生待证的性质,该文描述了一个Z的证明责任产生器的工作过程、完成证明责任产生器的工作难点就在于如何生成证明责任,本文对这一工作进行了详细的介绍。     

需求分析的 Z 语言形式化方法

非形式化的需求规格说明容易产生歧义,导致所开发的软件系统不能满足用户的功能要求.Z语言是一种基于集合和一阶谓词逻辑的模式规约语言,可用于产生精确的需求规格说明.介绍了需求分析的Z语言形式化方法,并给出了一个通用堆栈的Z语言描述实例,同时指出这种形式化方法有待进一步研究的地方.     

结构化面向对象形式规格说明语言OOZS——规格说明测试

自动或半自动实现面向对象形式规格说明的测试不但要求相应的规格说明语言具有严格的形式语义,而且要求使用人员具有较深的数学基础,从而最终影响了面向对象规格说明测试的研究。本文提出了一种测试方法,该方法通过构造测试用例对面向对象形式规格说明的各种特性进行检验,可以较容易地发现形式规格说明中的不一致、不完整之处。     

基于XML的用例规格说明实现

将XML技术应用到用例规格说明描述中,提出了基于XML的用例规格说明实现方法.使用XML Schema定义用例规格说明模板,并在此基础上产生用例规格说明的XML文件.实践证明,这样的描述方式具有规范和统一的特点,并能够自动检查语法.     

微机仿真系统中形式化方法的应用

Z语言是一种广泛应用的形式化语言，适合于仿真实时软件系统的需求规格说明．通过微机系统仿真软件的Z规格说明，讨论了Z语言在实时系统开发中使用的一些方法、对典型问题的处理原则以及操作同时序关系的描述．     

结构化面向对象形式规格说明语言OOZS——设计原理

形式方法与面向对象方法的综合使用可以使它们各自的优点得到充分体现：形式方法使目标软件系统的需求规格说明简明、精确,面向对象方法使目标软件系统的组织和分解工作更加系统、自然．本文讨论了Ｚ规格说明语言的应用限制,并在Ｚ语言的基础上介绍了结构化面向对象形式规格说明语言——ＯＯＺＳ的设计方法．该语言吸收了面向对象程序设计语言ＳｍａｌＴａｌｋ、Ｃ＋＋以及形式规格说明语言ＶＤＭ、Ｚｃ、Ｚ．Ｓ等的优点,引入了类、继承、入口、出口、Ｐｒｅ谓词、Ｐｏｓｔ谓词等机制,并对Ｚ语言的符号进行结构化处理,提高了形式规格说明的层次性和模块化能力,可用于大型面向对象软件系统需求规格说明的编写     

函数－规约混合语言的设计与实现

在函数式语言中引入约束类型和优化规则定义机制，并将扩展的函数式语言与代数规约说明语言相结合，支持从规约到程序的设计，并提高编程的效率及灵活性．混合语言系统将代数规约转换为合流的重写系统，将函数定义、计算约束和优化规则视为重写规则，基于重写模型，以平行最外方法辅以必要归约进行计算．     

基于ECC的程序规范描述

介绍一种扩展的类型理论构造演算ＥＣＣ；讨论了用它表示松散语义抽象类型的程序规范的方法，然后介绍如何用函数型语言ＭＬ使这种方法得以实现。     

基于VerilogHDL的数字集成电路高层设计环境

基于ＶｅｒｉｌｏｇＨＤＬ硬件描述语言以及ＶｅｒｉｌｏｇＸＬ模拟器，建立了从行为描述到寄存器传输级设计生成的数字集成电路高层设计环境，重点介绍了功能单元库的建立、目标硬件结构构成、排序与硬件配置。最后给出了一个设计实例。     

内含定理证明器的程序开发系统

提出了一个基于重写技术的程序开发系统,它提供了扩展的函数式语言和代数规约语言相结合的混合语言,该语言中引入了优化规则和测试等式说明机制．优化规则用于优化代码和满足某些特殊需求．运用测试等式说明机制可使程序员在程序中给出一些用于测试的等式,对程序进行测试,这些测试是在被开发系统形成前进行的．对优化规则和测试等式的证明,是由系统中的证明子系统（定理证明器）完成的．定理证明器的引入,提高了所开发系统的正确性,并且有利于缩短系统的开发周期．     

UML到SDL在地铁售票机系统中的应用

介绍了从统一建模语言(UML)到规范描述语言(SDL)的一种转化设计方法，并以地铁售票机系统的设计为例，介绍了具体的转化过程。售票机系统的需求规范用UML描述，系统的设计规范用SDL语言表示。     

模型驱动的Dafny程序形式化生成与自动验证

Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法; 然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式; 最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.     

Refinement and Transformation from Z Specification to C + +

As a kind of formal specification language, Z has gained a position in the field of software development, but there is still no standard way of transforming Z specification into executable code that is promising in increasing the quality, reusability and maintainability of software. With the automatic programming model of software engineering, through the analysis for Z specification language, a feasible semi-automatic way of refinement and transformation is proposed, and the correctness of the procedure is also discussed.     

基于Petri网的规范说明语言

对规范说明的研究是当前计算机科学领域的一个重要的课题,现已提出多种语言系统。本文从petri网的特点出发,提出了一种基于petri网的规范说明语言。首先介绍了它的数据类型,控制过程及实现方法,详细说明了网类型及其运算。最后还给出了一个具有实用价值的例子。