A Z Specification for Employment Clerical System

Z has become recognized as a very effective formal specification language in improving the quality of software and ensuring the cost effectiveness of the development process. This paper presents part of a case study of Z notations, ClericalTemps, which is an agency that provides a clerical help to its clients.

一种基于Z和精化演算的形式化开发方法

通过分析 Z和精化演算各自的特点 ,本文提出了一种使两者无缝集成的形式化开发方法 .该方法利用 Z良好的描述特性和扩充的类机制 ,将系统规约直接定义成精化演算中的抽象程序 ,然后用精化规则对抽象程序逐步精化 ,直到可执行程序 .

Z规格说明求精的正确性判定

软件求精是自动推理和形式化开发方法相结合而形成的一门新技术,它研究从抽象的形式格说明推演出具体的面向计算机的程序代码的全过程.其基本思想是用·个抽象程度低。

Z规格说明构造方法

比较完整地描述了Ｚ规格说明的结构和写规格说明的步骤，并通过一个所设计的Ｚ规格说明的实例演示了用Ｚ编写规格说明的过程。

基于Object-Z的UML对象模型的形式化

1 引言 UML作为面向对象的可视化建模语言,己被对象管理集团(OMG)作为面向对象分析和设计的标准,获得了众多工具的支持。UML提供了不同抽象层次的描述以支持面向对象的分析、设计和实施,它从不同的视图描述软件系统,减少了建模的复杂度,更为重要的是建立了基于元模型的体系结构,提供了较为灵活的扩充机制,使开发人员可以根据不同的领域需求定制UML,也易于加入新的建模概念。

一组实用的Z规格说明度量准则

众所周知,软件开发越到后期,为纠正或弥补错误所付出的代价会呈几何级数增长,因此规格说明的质量成为影响软件开发的难点和关键因素之一.为此,文中给出了一组针对形式规格说明语言Z模式的度量准则.该组准则考虑了模式修饰、模式包含、模式类型和模式出现在其他模式的变量说明和谓词约束部分的可能.根据这些度量准则,可以发现一些问题并把问题杜绝在软件开发的早期阶段,减少由于错误或不合理分析导致的浪费,并可对系统进行有效的评估.

结构化面向对象形式规格说明语言OOZS——应用实例

ＯＯＺＳ是一种面向对象的形式规格说明语言，它是Ｚ规格说明语言的一种面向对象扩展．本文结合一个四边形图形的例子对ＯＯＺＳ语言的应用进行说明．

规格说明语言Z的类型检查

软件规格说明的正确性是软件目标代码正确性的前提。正确性要求之一就是类型正确。本文介绍Z规格说明类型检查器的实现方法,并对类型检查的环境、一致化方法、替换策略和类型变量的应用等问题进行讨论。

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

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

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

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