| 致谢 | 第1-8页 |
| 摘要 | 第8-10页 |
| ABSTRACT | 第10-12页 |
| 目录 | 第12-16页 |
| 第0章 绪论 | 第16-21页 |
| ·引言 | 第16页 |
| ·形式化方法是软件开发方法合理的发展方向 | 第16-19页 |
| ·开发软件规格说明的目的 | 第16-17页 |
| ·软件语言作用 | 第17-18页 |
| ·软件语言低抽象级到高抽象级的发展 | 第18页 |
| ·规格说明的作用 | 第18-19页 |
| ·应用领域的要求 | 第19页 |
| ·影响形式方法使用的因素 | 第19-20页 |
| ·软件开发自动化程度不高。 | 第19-20页 |
| ·工业界的支持不够 | 第20页 |
| ·培养人才的目的不明确 | 第20页 |
| ·小结 | 第20-21页 |
| 第1章 结构化方法、面向对象方法和形式方法的比较 | 第21-30页 |
| ·引言 | 第21页 |
| ·三种方法的比较 | 第21-25页 |
| ·结构化与形式方法、面向对象与形式方法结合的不足 | 第25-26页 |
| ·结构化方法与面向对象方法的结合及问题 | 第26-28页 |
| ·FOO方法 | 第27页 |
| ·OOF方法 | 第27-28页 |
| ·结构化方法、面向对象方法、形式方法三者的结合 | 第28-29页 |
| ·小结 | 第29-30页 |
| 第2章 结构化面向对象的形式方法SOFM | 第30-37页 |
| ·引言 | 第30页 |
| ·SOFM思想 | 第30-31页 |
| ·结构化方法与面向对象方法的结合 | 第31-32页 |
| ·支持SOFM的一种实现 | 第32-36页 |
| ·SOZRSL方法 | 第32-33页 |
| ·SA和Object-Z作为SOZRSL基础的可行性 | 第33-34页 |
| ·数据流图与Obiect-Z的结合 | 第34页 |
| ·SOZRSL的逐步求精分解法 | 第34-35页 |
| ·SOZRSL的软件开发过程 | 第35-36页 |
| ·SOZRSL开发过程与传统开发过程的区别 | 第36页 |
| ·SOFM开发方法的优点 | 第36页 |
| ·小结 | 第36-37页 |
| 第3章 结构化object-Z需求规格说明语言SOZRSL | 第37-53页 |
| ·引言 | 第37页 |
| ·形式规格说明语言Z | 第37-39页 |
| ·Obiect-Z规格说明语言 | 第39-42页 |
| ·谓词数据流图 | 第42-46页 |
| ·谓词操作 | 第42-43页 |
| ·谓词数据流图(PDFD) | 第43页 |
| ·数据流 | 第43-44页 |
| ·谓词数据流图的输入、输出谓词操作和内部谓词操作 | 第44页 |
| ·谓词操作的分解 | 第44-45页 |
| ·分层谓词数据流图 | 第45-46页 |
| ·SOZRSL的系统结构 | 第46-48页 |
| ·SOZRSL的基本结构 | 第46-48页 |
| ·分层PDFD的继承 | 第48页 |
| ·SOZRSL的其他结构成分 | 第48页 |
| ·SOZRSL方法对传统方法的改进 | 第48-49页 |
| ·实例:培训中心系统 | 第49-52页 |
| ·小结 | 第52-53页 |
| 第4章 SOZRSL的公理化形式语义 | 第53-72页 |
| ·引言 | 第53页 |
| ·基本概念 | 第53-60页 |
| ·谓词操作 | 第54页 |
| ·数据流DF | 第54页 |
| ·谓词数据流图PDFD | 第54-57页 |
| ·分层谓词数据流图HPDFD | 第57-58页 |
| ·数据有效性 | 第58-59页 |
| ·一些约定 | 第59-60页 |
| ·语法约束 | 第60-61页 |
| ·PDFD有效性语义的公理化定义 | 第61-66页 |
| ·谓词操作的有效性语义 | 第62页 |
| ·谓词数据流图的有效性语义 | 第62-64页 |
| ·谓词操作的有效性分解 | 第64页 |
| ·有关定理的证明 | 第64-66页 |
| ·PDFD功能语义的公理化定义 | 第66-71页 |
| ·谓词操作的功能性语义 | 第66-68页 |
| ·谓词数据流图的功能性语义 | 第68-69页 |
| ·谓词操作的功能性分解 | 第69页 |
| ·功能语义的应用举例 | 第69-71页 |
| ·小结 | 第71-72页 |
| 第5章 SOZRSL的求精概述 | 第72-85页 |
| ·求精简介 | 第72-74页 |
| ·什么是求精 | 第72-73页 |
| ·几种常见求精的方法 | 第73-74页 |
| ·SOZRSL的求精 | 第74-81页 |
| ·SOZRSL的求精系统结构 | 第74-75页 |
| ·SOZRSL结构的求精 | 第75-76页 |
| ·SOZRSL的数据求精 | 第76-78页 |
| ·SOZRSL的谓词求精 | 第78-80页 |
| ·关于类和抽象数据类型的求精 | 第80-81页 |
| ·Guarded Command语言 | 第81-83页 |
| ·Guarded Command的语法 | 第82页 |
| ·岗哨语言的几种基本语句: | 第82-83页 |
| ·小结 | 第83-85页 |
| 第6章 基于程序综合的SOZRSL谓词求精 | 第85-103页 |
| ·基于程序综合的求精变换 | 第85-89页 |
| ·基本结构 | 第85-86页 |
| ·基本证明过程 | 第86-87页 |
| ·几点说明 | 第87页 |
| ·从SOZRSL规格说明到基本结构的变换 | 第87-89页 |
| ·求精变换中的规则和方法 | 第89-97页 |
| ·分解规则(splitting rule) | 第89-90页 |
| ·合并规则(merging rule) | 第90页 |
| ·重写规则 | 第90-92页 |
| ·归结(Resolution) | 第92-94页 |
| ·数学归纳法(mathematical induction) | 第94-96页 |
| ·构造辅助过程(Formation of Auxiliary Procedures) | 第96-97页 |
| ·控制优化策略和方法 | 第97-99页 |
| ·增加断言 | 第97页 |
| ·极性策略(Polarity Strategy) | 第97-98页 |
| ·遗传算法 | 第98页 |
| ·求精过程和结果的重用 | 第98-99页 |
| ·求精中的模式演算 | 第99-102页 |
| ·对模式与运算的求精 | 第99-101页 |
| ·对模式或运算的求精 | 第101-102页 |
| ·小结 | 第102-103页 |
| 第7章 遗传算法用于SOZRSL求精中的规则选择 | 第103-114页 |
| ·进化计算 | 第103-105页 |
| ·遗传算法简介 | 第104页 |
| ·遗传算法的主要步骤 | 第104-105页 |
| ·应用遗传算法在求精过程中选择规则 | 第105-110页 |
| ·规则的表示 | 第105-106页 |
| ·规则的编码 | 第106-108页 |
| ·适应值的度量 | 第108-109页 |
| ·编码的交叉方式 | 第109-110页 |
| ·确定控制参数与停机准则 | 第110页 |
| ·一个简单的实例 | 第110-113页 |
| ·小结 | 第113-114页 |
| 第8章 求精变换的机器实现 | 第114-128页 |
| ·系统开发环境 | 第114页 |
| ·SOZRSL求精变换系统结构 | 第114-115页 |
| ·基于推理的程序综合求精变换系统结构 | 第115-116页 |
| ·系统的分析、设计实现 | 第116-127页 |
| ·类的建立 | 第116页 |
| ·类的设计 | 第116-125页 |
| ·求精的执行过程 | 第125-126页 |
| ·主要的界面 | 第126-127页 |
| ·小结 | 第127-128页 |
| 第9章 可视化的SOZRSL编辑器的设计与实现 | 第128-142页 |
| ·SOZRSL编辑器的用户界面及环境要求 | 第128-129页 |
| ·使用说明 | 第129页 |
| ·SOZRSL编辑器的功能要求 | 第129页 |
| ·系统构成 | 第129-130页 |
| ·类的设计与实现 | 第130-139页 |
| ·Text类 | 第131页 |
| ·SozToText类 | 第131-132页 |
| ·Page类 | 第132-133页 |
| ·Block类 | 第133页 |
| ·Pragraph类 | 第133-134页 |
| ·Name类、Declare类和Predict类 | 第134页 |
| ·Schema类 | 第134-135页 |
| ·PDFD类 | 第135页 |
| ·TextLine类 | 第135-139页 |
| ·SOZRSL编辑器关键技术的实现 | 第139-141页 |
| ·特殊字符的实现 | 第139页 |
| ·上标与下标的实现 | 第139-140页 |
| ·汉字的处理 | 第140页 |
| ·关于注释 | 第140-141页 |
| ·小结 | 第141-142页 |
| 结束语 | 第142-144页 |
| 附录 SOZRSL语法 | 第144-151页 |
| 参考文献 | 第151-159页 |
| 作者在攻读博士学位期间发表和录用的论文 | 第159-160页 |
| 作者在攻读博士学位期间参与的科研项目及获奖情况 | 第160页 |
