| 摘要 | 第1-8页 |
| ABSTRACT | 第8-10页 |
| 目录 | 第10-13页 |
| 第一章 绪论 | 第13-24页 |
| ·软件测试概述 | 第13-14页 |
| ·测试充分性准则 | 第14-16页 |
| ·基于规格说明的软件测试 | 第16-18页 |
| ·形式方法和形式规格说明 | 第16-17页 |
| ·基于模型规格说明的软件测试 | 第17页 |
| ·基于代数规格说明的软件测试 | 第17-18页 |
| ·基于有限状态机的测试 | 第18页 |
| ·面向对象的软件测试 | 第18-23页 |
| ·面向对象测试面临的主要问题及相关的工作 | 第19-22页 |
| ·基于规格说明的面向对象软件测试 | 第22-23页 |
| ·相关术语 | 第23页 |
| ·论文大纲 | 第23-24页 |
| 第二章 对逻辑覆盖准则的公理化评估 | 第24-37页 |
| ·逻辑覆盖准则 | 第25-29页 |
| ·谓词覆盖和文字覆盖 | 第26-27页 |
| ·活动文字覆盖 | 第27-29页 |
| ·逻辑覆盖准则的公理系统 | 第29-33页 |
| ·有限可应用性、单调性和空集不充分性 | 第29-30页 |
| ·最小固定尺寸性质 | 第30-31页 |
| ·充分测试集的完全性 | 第31-32页 |
| ·代表性 | 第32-33页 |
| ·相关性 | 第33页 |
| ·评估 | 第33-36页 |
| ·有限可应用性、空集不充分性和单调性 | 第34页 |
| ·最小固定尺寸性质 | 第34-35页 |
| ·完全性 | 第35页 |
| ·代表性 | 第35页 |
| ·相关性 | 第35-36页 |
| ·小结 | 第36-37页 |
| 第三章 基于形式规格说明的类测试准则 | 第37-52页 |
| ·类内部测试准则 | 第37-45页 |
| ·全测试覆盖 | 第40页 |
| ·全无环有效序列覆盖 | 第40-43页 |
| ·最大无环有效序列覆盖 | 第43-44页 |
| ·类内部测试准则之间的包含关系 | 第44-45页 |
| ·实例研究 | 第45-48页 |
| ·Object-Z类规格说明 | 第45-47页 |
| ·测试用例生成 | 第47-48页 |
| ·测试结果和分析 | 第48-51页 |
| ·构造基于状态图的测试用例 | 第48-49页 |
| ·评估 | 第49-51页 |
| ·小结 | 第51-52页 |
| 第四章 基于形式规格说明的测试类框架 | 第52-65页 |
| ·测试类框架 | 第53-59页 |
| ·构造测试用例的方法 | 第53-56页 |
| ·描述测试用例产生的过程 | 第56-59页 |
| ·实例研究 | 第59-64页 |
| ·小结 | 第64-65页 |
| 第五章 基于形式规格说明的多态关系的测试 | 第65-82页 |
| ·基于规格说明的多态测试准则 | 第66-78页 |
| ·测试操作中的多态对象 | 第66-71页 |
| ·测试类中的多态对象 | 第71-78页 |
| ·实例分析 | 第78-81页 |
| ·小结 | 第81-82页 |
| 第六章 测试类框架的继承扩充 | 第82-96页 |
| ·继承和OBJECT-Z | 第83-87页 |
| ·实例 | 第83-85页 |
| ·Object-Z中的继承语义 | 第85-87页 |
| ·子类测试框架的推导 | 第87-95页 |
| ·方法内测试过程框架的重用 | 第87-93页 |
| ·类内部测试框架的重用 | 第93-95页 |
| ·小结 | 第95-96页 |
| 第七章 从测试用例规格说明到测试数据生成 | 第96-104页 |
| ·线性规划 | 第96-97页 |
| ·求解非线性不等式的策略 | 第97-103页 |
| ·小结 | 第103-104页 |
| 第八章 系统的实现 | 第104-113页 |
| ·系统的总体框架 | 第104-105页 |
| ·用例的实现 | 第105-112页 |
| ·Obiect-Z编辑器 | 第105-107页 |
| ·语法分析器的设计与实现 | 第107-108页 |
| ·方法内测试用例生成模块的设计和实现 | 第108-110页 |
| ·测试用例具体化模块的设计和实现 | 第110-112页 |
| ·类内部测试用例生成模块的设计与实现 | 第112页 |
| ·小结 | 第112-113页 |
| 第九章 结束语 | 第113-116页 |
| ·本文主要贡献 | 第113-114页 |
| ·将来的工作 | 第114-116页 |
| 参考文献 | 第116-119页 |
| 附录一 VENDINGMACHINE的方法内测试用例 | 第119-121页 |
| 附录二 VENDINGMACHINE的类内部测试用例 | 第121-124页 |
| 附录三 类VENDINGMACHINE的代码 | 第124-127页 |
| 附录四 TETRIS系统的实现代码 | 第127-148页 |
| 作者在攻读博士学位期间发表和录用的论文 | 第148页 |
| 作者在攻读博士期间参与的科研项目及获奖情况 | 第148-149页 |
| 致谢 | 第149页 |