绪论 1
第一章 结构化方法、面向对象方法和形式方法的比较 8
1.1 引言 8
1.2 三种方法的比较 9
1.3 结构化与形式方法、面向对象与形式方法结合的不足 14
1.4 结构化方法与面向对象方法的结合及问题 15
1.5 结构化方法、面向对象方法、形式方法三者的结合 18
1.6 小结 20
第二章 结构化面向对象的形式方法SOFM 21
2.1 引言 21
2.2 SOFM思想 22
2.3 结构化方法与面向对象方法的结合 23
2.4 支持SOFM的一种实现 25
2.5 SOFM开发方法的优点 30
2.6 小结 31
第三章 结构化Object-Z需求规格说明语言SOZRSL 32
3.1 引言 32
3.2 形式规格说明语言Z 32
3.3 Object-Z规格说明语言 35
3.4 谓词数据流图 40
3.5 SOZRSL的系统结构 45
3.6 SOZRSL方法对传统方法的改进 49
3.7 实例：培训中心系统 50
3.8 小结 54
第四章 SOZRSL的公理化形式语义 56
4.1 引言 56
4.2 基本概念 57
4.3 语法约束 68
4.4 PDFD有效性语义的公理化定义 70
4.5 PDFD功能语义的公理化定义 77
4.6 小结 84
第五章 SOZRSL的求精概述 85
5.1 求精简介 85
5.2 SOZRSL的求精 89
5.3 Guarded Command语言 100
5.4 小结 103
第六章 基于程序综合的SOZRSL谓词求精 104
6.1 基于程序综合的求精变换 104
6.2 求精变换中的规则和方法 110
6.3 控制优化策略和方法 123
6.4 求精中的模式演算 126
6.5 小结 130
第七章 遗传算法用于SOZRSL求精中的规则选择 131
7.1 进化计算 131
7.2 应用遗传算法在求精过程中选择规则 135
7.3 一个简单的实例 142
7.4 小结 146
第八章 求精变换的机器实现 148
8.1 系统开发环境 148
8.2 SOZRSL求精变换系统结构 148
8.3 基于推理的程序综合求精变换系统结构 149
8.4 系统的分析、设计实现 151
8.5 小结 171
第九章 可视化的SOZRSL编辑器的设计与实现 172
9.1 SOZRSL编辑器的用户界面及环境要求 172
9.2 使用说明 173
9.3 SOZRSL编辑器的功能要求 173
9.4 系统构成 174
9.5 类的设计与实现 175
9.6 SOZRSL编辑器关键技术的实现 189
9.7 小结 191
第十章 结束语 193
附录 SOZRSL语法 196
参考文献 209
致谢 222