Z形式规约的自动求精研究

第1章Z形式规约

1.1软件开发的形式化方法

1.1.1形式化方法的意义

1.1.2Z形式规约的产生与发展

1.1.3Z形式规约的特点

1.2Z形式规约的类型

1.2.1Z形式规约中的基本数据类型

1.2.2Z形式规约中的复合数据类型

1.3Z形式规约的构造单元

1.3.1Z形式规约的符号

1.3.2Z形式规约的模式

1.4Z形式规约的关系和函数

1.4.1关系

1.4.2数

1.5Z形式规约求精技术

1.5.1软件求精的概念

1.5.2Z形式规约的软件体系结构

1.5.3求精过程

1.5.4Z形式规约自动求精的研究

第2章C++标准模板库STL

2.1STL简介

2.2STL基本结构

2.3容器

2.4迭代器

2.5算法

2.6其他组件

第3章Z形式规约的精简SmartZ

3.1概述

3.2Z形式规约的类型约束

3.2.1Z形式规约约束和可判定性

3.2.2约束问题的提出

3.2.3Z形式规约的类型约束

3.3Z形式规约的谓词约束

3.3.1谓词的约束与可判定性

3.3.2谓词与模式的可扩展性

3.4Z形式规约的精简

3.4.1形式语言的描述

3.4.2SmartZ的词法

3.4.3SmartZ文法设计

第4章SmartZ的自动求精

4.1SmartZ的词法分析

4.1.1扫描器

4.1.2词法分析

4.1.3词法分析的流程

4.1.4表达式的处理

4.1.5组合运算符处理的流程

4.1.6中文字符处理

4.1.7其他字符

4.1.8出错处理

4.2SmartZ的语法分析

4.2.1SmartZ语法分析阶段

4.2.2SmartZ文法范式的确定

4.2.3语法转换规则

4.2.4程序图形化设计方法

4.2.5从语法图到SI－NI图的转换法则

4.2.6语法分析程序的实现

4.2.7语法出错处理

4.3SmartZ的语义分析

4.3.1符号表的设计

4.3.2语义树的建立

4.3.3变量声明的语义分析与求精

4.4SmartZ的自动求精转换器

4.4.1SmartZ的自动求精过程

4.4.2从规格说明到程序代码的自动求精

第5章一阶逻辑算子的自动求精

5.1一阶逻辑

5.2一阶逻辑算子的自动求精步骤

5.3表达式处理

5.3.1算术表达式和逻辑表达式

5.3.2表达式向逆波兰式的转换算法

5.4SmartZ的量词与连接词的自动求精

5.4.1全称量词和存在量词

5.4.2连接词

5.4.3赋值语句

5.5一阶逻辑算子的目标代码生成

5.5.1语义分析与求精过程

5.5.2一阶逻辑算子的目标代码顺序

5.5.3出错处理

5.6一个模式求精实例

第6章集合论算子的自动求精

6.1集合类型的声明

6.2目标代码中的集合操作

6.3集合论算子到中间代码的转换

6.4采用模板及重载技术设计SmartZ中集合论算子的求精

6.4.1采用模板实现SmartZ算子的自动求精

6.4.2运算符重载在SmartZ算子自动求精中的应用

6.4.3SmartZ中集合论算子自动求精的具体算法

6.5集合论算子自动求精实例

6.5.1图书馆数据库管理的规格说明

6.5.2用于自动求精的规格说明

6.5.3转换为C++程序代码

第7章幂集算子的自动求精

7.1幂集类型

7.2广义表

7.2.1广义表的定义

7.2.2广义表的存储结构

7.3单层幂集的自动求精

7.4多层嵌套幂集的自动求精

7.5幂集的自动求精实例

第8章笛卡儿积的自动求精

8.1笛卡儿积的声明

8.2笛卡儿积的数据求精

8.3笛卡儿积的过程求精

8.4笛卡儿积的自动求精实例

第9章关系和函数的自动求精

9.1序偶与关系

9.1.1序偶

9.1.2关系

9.2关系操作与自动求精

9.2.1SmartZ的关系操作及中间代码

9.2.2SmartZ关系操作实例

9.3函数操作与自动求精

9.3.1函数

9.3.2函数操作的中间代码与自动求精

第10章序列和包的自动求精

10.1序列和包

10.1.1序列

10.1.2包

10.2序列操作的自动求精

10.2.1序列的个数

10.2.2序列的连接操作

10.2.3序列的逆置操作

10.2.4序列的查找操作

10.2.5序列的head操作

10.2.6序列的last操作

10.2.7序列的tail操作

10.2.8序列的front操作

10.2.9序列的抽取

10.2.10序列的过滤

10.2.11序列的压缩

10.2.12序列的划分

10.3包操作的自动求精

10.3.1C++STL中的map容器

10.3.2包的计数操作

10.3.3计算包中任意元素个数的操作

10.3.4包的扩大操作

10.3.5判断元素是否为包的成员操作

10.3.6判断子包关系的操作

10.3.7给定序列返回包的操作

10.3.8包的和函数操作

10.3.9包的减函数操作

10.4序列和包的自动求精实例

附录1Z语法

附录2SmartZ词法

附录3SmartZ的词法DFA

附录4SmartZ语法

附录5SmartZ语法的部分SI－NS图

附录6部分SmartZ算子的函数模板

参考文献

　　本书共10章和6个附录。第1章介绍了形式化软件开发的意义、Z形式规约的诞生与发展、Z形式规约的体系以及本书研究的内容和意义。第2章介绍了本书自动求精的目标代码体系C++代码和STL标准模板库。第3章，通过理论推导，证明了Z形式规约经过适当的约束后，其一阶逻辑算子的自动求精是可以实现的。第4章研究了SmartZ自动求精的整体过程。第5章讨论了一阶逻辑表达式的处理方法，给出了一阶逻辑算子包括量词和连接词的自动求精技术。第6章结合C++语言的模板、重载技术和STL模板库对数据结构和通用算法的强大支持功能。第7章通过对幂集类型以及结构的深入分析，找到与之相似的STL容器的存储结构与数据结构，讨论了幂集类型在自动求精过程中的实现方式，并给出在求精过程中的算法以及规则。第8章研究了笛卡儿积算子的数据求精和过程求精。第9章研究了关系和函数的存储、关系和函数转换为中间代码的方法，设计了中间代码的自定义函数，实现了全入射函数、部分入射函数、全满射函数和部分满射函数的自动求精。第10章利用C++及STL技术设计了序列和包各种操作的求精规则，并产生目标程序，即把Z规格说明转换为C++代码，实现了序列和包的自动求精。