《软件形式规格说明语言-Z》 缪淮扣

第一章  绪论

1.1 软件生命周期：  需求分析与规格说明 设计 实现 测试 交付与维护 ——瀑布模型

1.2 软件规格说明的两种抽象：过程抽象、数据抽象。过程抽象描述软件系统要实现的功能，而不是如何实现的具体步骤；数据抽象就是在规格说明中使用集合、关系、映射、序列、包等抽象的数学结构。

为了克服自然语言和程序设计语言描述规格说明的缺陷，人们提出了一种新的软件开发范型，即通过形式化、规范化的数学理论，用描述“做什么”取代“怎么做”。

包含两种技术：形式规格说明技术  形式验证技术 都基于数学基础，集合论 逻辑 代数理论等

1.3 形式规格说明语言的分类：

基于模型——基本思想利用一些已知的特性的数学抽象来为目标软件系统的状态特性和行为特性构造模型。数学抽象包括域、元组、集合、序列、包、映射等。 Z VDM B

代数方法——通过提供一些特殊机制以允许对目标软件系统描述的结构化，并支持目标软件系统中公共元素的重用。仅使用带有等词的一阶逻辑表示，不引入通常的数学对象。 ACT ONE   CLEAR OBJ Larch

进程代数——采用代数方法对并行或分布式系统进行研究的方法。提供了用于描述进程的规格说明的代数语言。提供了描述并发系统所需的并行复合、选择、顺序复合等语句，并可通过等式推理的方法来验证系统满足某些性质。 CSP CCS LOTOS

1.4 Z语言概述

Z语言是基于一阶谓词逻辑和集合论的形式规格说明语言。采用了严格的数学理论，可以产生简明、精确、无歧义且可证明的规格说明。Z语言的主要特点是可以对Z规格说明进行推理和证明。使得软件开发人员或用户能够很快找出规格说明的不一致、不完整之处，提供对软件的信心。

将Z语言称为规格说明语言的关键思想是把软件开发中的需求规格说明阶段和软件设计阶段分开。

Z语言方法学，强调“描述性”思维，忽略过程强调功能描述的技术称为过程抽象或者操作抽象。

《软件形式规格说明语言-Z》 缪淮扣 学习笔记 10-12