第1章 绪论 1
1.1 形式化方法概述 1
1.1.1 形式化方法的概念 1
1.1.2 形式化方法的必要性 2
1.1.3 系统设计错误 4
1.1.4 形式化方法的分类 5
1.2 Z语言概述 5
1.2.1 Z语言的创始人 6
1.2.2 Z语言的简史 6
1.2.3 Z语言的规范 6
1.3 Z语言的特点 7
1.4 Z语言的数学基础 7
1.5 Z语言的词汇 9
1.6 总结 9
第2章 集合 10
2.1 符号和基数以及成员关系 10
2.2 不变集合与可变集合 11
2.3 韦恩图 11
2.4 集合的运算 12
2.4.1 并集合 12
2.4.2 交集合 13
2.4.3 差集合 15
2.5 集合的表示 16
2.5.1 枚举法和图形法 16
2.5.2 集合的谓词表示法 16
2.5.3 描述类型的集合 17
2.5.4 集合的模式表示法 18
2.5.5 集合的谓词和模式的混合表示法 19
2.6 集合词汇 19
2.7 总结 20
第3章 命题 21
3.1 真假命题 21
3.2 复合命题 21
3.2.1 逻辑合取 21
3.2.2 逻辑析取 22
3.2.3 逻辑否定 23
3.3 真值表 24
3.4 逻辑联结词的优先级 26
3.5 等价集合与子集合 27
3.5.1 等价集合 28
3.5.2 子集合 28
3.6 幂集 29
3.7 笛卡儿积 31
3.8 扩展类型 32
3.9 蕴含联结词和等价联结词 33
3.9.1 蕴含联结词 33
3.9.2 等价联结词 35
3.10 常见的等价推理 35
3.11 总结 36
第4章 模式 38
4.1 规约 38
4.2 磁盘收集盒问题 39
4.2.1 对象 39
4.2.2 状态模式 40
4.2.3 操作模式 41
4.2.4 报错模式 43
4.2.5 初始化模式 44
4.3 酒店客房问题 45
4.4 总结 49
第5章 函数表达式 50
5.1 函数的基本概念 50
5.2 部分函数与全函数 52
5.3 全入射函数与部分入射函数 53
5.4 全满射函数与部分满射函数 54
5.5 双射函数 55
5.6 总结 56
第6章 谓词 57
6.1 谓词 57
6.2 全称量词 57
6.3 存在量词 58
6.4 只存在一个 59
6.5 命题以及谓词的应用 59
6.6 总结 61
第7章 关系 62
7.1 关系的定义 62
7.2 关系和笛卡儿积 63
7.3 关系-笛卡儿积（不仅是比对） 64
7.4 关系的定义域和值域 64
7.5 定义域限定 66
7.6 定义域反限定 67
7.7 值域限定 69
7.8 值域反限定 69
7.9 关系复合 70
7.10 关系的逆运算 73
7.11 总结 74
第8章 Z语言的使用实例 75
8.1 学生宿舍管理系统案例 75
8.2 贪吃蛇小游戏 82
8.2.1 游戏的简单规则 82
8.2.2 游戏系统的界面 83
8.2.3 游戏胜负判断 83
8.2.4 子函数与变量 84
8.3 总结 92
第9章 Z语言的使用 94
9.1 常用的Z语言描述工具 94
9.1.1 业界Z工具 95
9.1.2 形式化方法软件Z/EVES 95
9.1.3 LaTex格式的Z语言辅助工具 95
9.1.4 Z Word Tools 96
9.2 Z语言的使用方法 97
9.2.1 Z独立系统 97
9.2.2 Z集成插件 97
9.2.3 Z接口模块 98
9.2.4 规范包装 98
9.3 总结 98
第10章 Z规格说明生成器 100
10.1 Z规格说明自动生成器实现 100
10.1.1 输入区域 100
10.1.2 显示区域 102
10.2 Z规格说明自动生成器的演示 104
10.2.1 问题说明 104
10.2.2 初始化模式 104
10.2.3 增加联系人 106
10.2.4 删除联系人 108
10.2.5 修改联系人电话 110
10.3 总结 112
参考文献 113
附录1 Z语言词汇表 116
附录2 Z语言技术术语汉英对照表 123
附录3 Z语言演算符号一览表 128
附录4 LaTex命令和Z语言对应表 134
附录5 Z语言术语索引表 141
致谢 145