Z形式规约是一种世界上广泛使用的软件规格说明语言，在软件开发的需求规格说明阶段和软件设计阶段都可以使用，对于提高大型软件质量、验证软件设计正确性等方面具有非常重要的意义。
由于Z是以集合论和一阶逻辑为基础，是设计用来给人看的而不能由机器执行。将Z转换成高级语言需要专业的数学知识，而且对于大型软件，转换过程极易出错。Z的机器可执行性已经引起世界范围的关注，但目前还不能直接从Z语言自动生成应用程序，Z到可执行代码的转换主要由人工完成。本书指出了Z语言求精方法对于自动生成应用程序的不足，提出了对Z规格说明做一定限制后的Smart Z自动求精为C++和STL方法。
　　本书叙述简明清晰，逻辑性强，可作为高等学校相关专业研究生和从事形式语言研究、大型软件形式化开发与应用的专业人员参考。

第1章 Z形式规约
1.1 软 件开发的形式化方法
1.2 Z形式规约的类型
1.3 Z形式规约的构造单元
1.4 Z形式规约的关系和函数
1.5 Z形式规约求精技术
第2章 ++标准模板库STL
　2.1 STL简介
　2.2 STL基本结构
　2.3 容器
　2.4 迭代器
　2.5 算法
　2.6 其他组件
第3章 Z形式规约的精简—Smart Z
　3.1 概述
　3.2 Z形式规约的类型约束
　3.3 Z形式规约的谓词约束
　3.4 Z形式规约的精简
第4章 Smart Z的自动求精
　4.1 Smart Z的词法分析
　4.2 Smart Z的语法分析
　4.3 Smart Z的语义分析
　4.4 Smart Z的自动求精转换器
第5章 一阶逻辑算子的自动求精
　5.1 一阶逻辑
　5.2 一阶逻辑算子的自动求精步骤
　5.3 表达式处理
　5.4 Smart Z的量词与连接词的自动求精
　5.5 一阶逻辑算子的目标代码生成
　5.6 一个模式求精实例
第6章 集合论算子的自动求精
　6.1 集合类型的声明
　6.2 目标代码中的集合操作
　6.3 集合论算子到中间代码的转换
　6.4 采用模板及重载技术设计Smart Z中集合论算子的求精
　6.5 集合论算子自动求精实例
第7章 幂集算子的自动求精
　7.1 幂集类型
　7.2 广义表
　7.3 单层幂集的自动求精
　7.4 多层嵌套幂集的自动求精
　7.5 幂集的自动求精实例
第8章 笛卡儿积的自动求精
　8.1 笛卡儿积的声明
　8.2 笛卡儿积的数据求精
　8.3 笛卡儿积的过程求精48
　8.4 笛卡儿积的自动求精实例
第9章 关系和函数的自动求精
　9.1 序偶与关系
　9.2 关系操作与自动求精
　9.3 函数操作与自动求精
第10章 序列和包的自动求精
　10.1 序列和包
　10.2 序列操作的自动求精
　10.3 包操作的自动求精
　10.4 序列和包的自动求精实例
附录1 Z语法
附录2 Smart Z词法
附录3 Smart Z的词法
附录4 Smart Z语法
附录5 Smart Z语法的部分SI-NS图
附录6 部分Smart Z算子的函数模板
参考文献

第1章　z形式规约
　　1.1 软件开发的形式化方法
　　1.1.1　形式化方法的意义
软件开发的过程是从对用户的需求进行分析开始的，经过设计和实现，最后产生可以正确执行的代码以及有关使用和维护的各种文档。完成这个过程的方法称为软件开发方法。
传统的软件开发方法引入一些非形式的图形和文字符号，提供一定的设计原则，协助开发人员按照一定的步骤，比较明确和简练地书写设计文档，用人工方式开发出所要的软件。从各软件加工模型来看，用户需求的规格说明在软件开发过程中具有非常重要的地位。其使用者包括用户、系统分析员、设计与编程人员、测试和验收人员。
许多软件项目开发的经验表明，软件开发费用的大部分是用于纠正在测试阶段所发现的各种错误。而更详细的调查告诫我们，这些错误中的很大一部分可追溯到项目开发的早期阶段，即在实现和测试阶段所花的高额费用是由于需求分析和设计阶段虚假的“节省”所引起的。需求分析阶段的错误通常就是规格说明的描述不精确。
众所周知，采用自然语言描述的非形式的规格说明具有易读、易理解的优点，但它通常具有模糊性和歧义性（二义性），经常是不精确和不完整的。这往往引起规格说明的使用者对同一规格说明产生不同的理解，最终导致用户对已完成的系统不满意。
　　……