第1章 Z形式规约 1
1．1软件开发的形式化方法 1
形式化方法的意义 1
Z形式规约的产生与发展 4
Z形式规约的特点 8
1．2 Z形式规约的类型 9
Z形式规约中的基本数据类型 10
Z形式规约中的复合数据类型 11
1．3 Z形式规约的构造单元 14
Z形式规约的符号 14
Z形式规约的模式 15
1．4 Z形式规约的关系和函数 16
关系 16
函数 19
1．5 Z形式规约求精技术 21
软件求精的概念 21
Z形式规约的软件体系结构 21
求精过程 24
Z形式规约自动求精的研究 29
第2章 C＋＋标准模板库STL 33
2．1 STL简介 33
2．2 STL基本结构 34
2．3容器 36
2．4迭代器 40
2．5算法 40
2．6其他组件 41
第3章 Z形式规约的精简—Smart Z 44
3．1概述 44
3．2 Z形式规约的类型约束 45
Z形式规约约束和可判定性 45
约束问题的提出 46
Z形式规约的类型约束 47
3．3 Z形式规约的谓词约束 52
谓词的约束与可判定性 52
谓词与模式的可扩展性 54
3．4 Z形式规约的精简 55
形式语言的描述 55
Smart Z的词法 59
Smart Z文法设计 61
第4章 Smart Z的自动求精 71
4．1 Smart Z的词法分析 71
扫描器 71
词法分析 72
词法分析的流程 75
表达式的处理 75
组合运算符处理的流程 77
中文字符处理 78
其他字符 78
出错处理 78
4．2 Smart Z的语法分析 79
Smart Z语法分析阶段 79
Smart Z文法范式的确定 79
语法转换规则 82
程序图形化设计方法 84
从语法图到SI-NI图的转换法则 87
语法分析程序的实现 89
语法出错处理 95
4．3 Smart Z的语义分析 96
符号表的设计 97
语义树的建立 99
变量声明的语义分析与求精 101
4．4 Smart Z的自动求精转换器 105
Smart Z的自动求精过程 106
从规格说明到程序代码的自动求精 108
第5章 一阶逻辑算子的自动求精 111
5．1一阶逻辑 111
5．2一阶逻辑算子的自动求精步骤 112
5．3表达式处理 113
算术表达式和逻辑表达式 114
表达式向逆波兰式的转换算法 115
5．4 Smart Z的量词与连接词的自动求精 117
全称量词和存在量词 118
连接词 119
赋值语句 119
5．5一阶逻辑算子的目标代码生成 120
语义分析与求精过程 120
一阶逻辑算子的目标代码顺序 124
出错处理 125
5．6一个模式求精实例 126
第6章 集合论算子的自动求精 131
6．1集合类型的声明 131
6．2目标代码中的集合操作 132
6．3集合论算子到中间代码的转换 133
6．4采用模板及重载技术设计Smart Z中集合论算子的求精 140
采用模板实现Smart Z算子的自动求精 140
运算符重载在Smart Z算子自动求精中的应用 141
Smart Z中集合论算子自动求精的具体算法 143
6．5集合论算子自动求精实例 144
图书馆数据库管理的规格说明 144
用于自动求精的规格说明 145
转换为C＋＋程序代码 146
第7章 幂集算子的自动求精 149
7．1幂集类型 149
7．2广义表 151
广义表的定义 151
广义表的存储结构 152
7．3单层幂集的自动求精 153
7．4多层嵌套幂集的自动求精 155
7．5幂集的自动求精实例 158
第8章 笛卡儿积的自动求精 161
8．1笛卡儿积的声明 161
8．2笛卡儿积的数据求精 161
8．3笛卡儿积的过程求精 164
8．4笛卡儿积的自动求精实例 166
第9章 关系和函数的自动求精 172
9．1序偶与关系 172
序偶 172
关系 173
9．2关系操作与自动求精 174
Smart Z的关系操作及中间代码 174
Smart Z关系操作实例 175
9．3函数操作与自动求精 179
函数 179
函数操作的中间代码与自动求精 179
第10章 序列和包的自动求精 187
10．1序列和包 187
序列 187
包 189
10．2序列操作的自动求精 190
序列的个数 190
序列的连接操作 191
序列的逆置操作 193
序列的查找操作 193
序列的head操作 194
序列的last操作 194
序列的tail操作 195
序列的front操作 195
序列的抽取 196
序列的过滤 197
序列的压缩 197
序列的划分 198
10．3包操作的自动求精 199
C＋＋STL中的map容器 199
包的计数操作 201
计算包中任意元素个数的操作 202
包的扩大操作 203
判断元素是否为包的成员操作 203
判断子包关系的操作 204
给定序列返回包的操作 205
包的和函数操作 205
包的减函数操作 206
10．4序列和包的自动求精实例 207
附录1 Z语法 209
附录2 Smart Z词法 214
附录3 Smart Z的词法DFA 215
附录4 Smart Z语法 216
附录5 Smart Z语法的部分SI-NS图 220
附录6 部分Smart Z算子的函数模板 223
参考文献 228