| 摘要 | 第1-8页 |
| Abstract | 第8-12页 |
| 第一章 序论 | 第12-18页 |
| ·研究背景 | 第12-16页 |
| ·使用UML进行系统设计 | 第13-14页 |
| ·UML作为ADL | 第14-15页 |
| ·问题总结 | 第15-16页 |
| ·解决方案 | 第16-17页 |
| ·JML | 第16页 |
| ·OCL-JML转换 | 第16-17页 |
| ·JML-AddIn工具 | 第17页 |
| ·本文的主要贡献 | 第17页 |
| ·本文的组织结构 | 第17-18页 |
| 第二章 基于OCL-JML转换的解决方案 | 第18-27页 |
| ·OCL | 第19-21页 |
| ·JML及其支撑工具 | 第21-23页 |
| ·JML | 第21-22页 |
| ·JML的支撑工具 | 第22-23页 |
| ·OCL-JML转换的意义 | 第23-24页 |
| ·OCL-JML转换的可行性分析 | 第24-25页 |
| ·OCL和JML都是强类型语言 | 第24-25页 |
| ·OCL和JML的断言和表达式都是虚的(pure) | 第25页 |
| ·OCL和JML都是DBC语言 | 第25页 |
| ·小结 | 第25-27页 |
| 第三章 OCL-JML映射机制 | 第27-45页 |
| ·OCL抽象语法树 | 第27-28页 |
| ·基本数据类型的映射机制 | 第28-29页 |
| ·基本操作表达式 | 第28页 |
| ·布尔类型 | 第28-29页 |
| ·其他类型 | 第29页 |
| ·属性表达式 | 第29-30页 |
| ·导航表达式 | 第29-30页 |
| ·集合操作的映射机制 | 第30-37页 |
| ·等价的映射机制 | 第31-32页 |
| ·公共操作的映射机制 | 第32-33页 |
| ·Set类型的操作符的映射机制 | 第33-35页 |
| ·Bag类型的操作符的映射机制 | 第35-36页 |
| ·Sequence操作符的映射机制 | 第36-37页 |
| ·迭代表达式的映射机制 | 第37-38页 |
| ·其他OCL结构的映射机制 | 第38-40页 |
| ·约束的转换机制 | 第40-44页 |
| ·上下文表达式 | 第40-41页 |
| ·方法规范的转换机制 | 第41-43页 |
| ·类规范的转换机制 | 第43-44页 |
| ·小结 | 第44-45页 |
| 第四章 JML-AddIn工具的实现框架 | 第45-51页 |
| ·Rational Rose系列建模工具的优点 | 第45-46页 |
| ·Rational Rose工具的扩展接口 | 第46页 |
| ·JML-AddIn工具的实现框架 | 第46-50页 |
| ·用户界面 | 第47-48页 |
| ·接口模块 | 第48页 |
| ·OCL语法检查工具 | 第48-49页 |
| ·JML代码翻译器 | 第49-50页 |
| ·小结 | 第50-51页 |
| 第五章 应用实例 | 第51-61页 |
| ·实例描述 | 第51-55页 |
| ·用例图 | 第51-52页 |
| ·类图 | 第52-53页 |
| ·接口 | 第53-55页 |
| ·实例中JML-AddIn工具的应用 | 第55-59页 |
| ·约束添加 | 第55-58页 |
| ·代码生成 | 第58-59页 |
| ·高层设计对下层实现的指导 | 第59页 |
| ·自动化测试 | 第59页 |
| ·小结 | 第59-61页 |
| 第六章 总结与展望 | 第61-64页 |
| ·本文总结 | 第61-62页 |
| ·相关工作和展望 | 第62-64页 |
| 第七章 参考文献 | 第64-66页 |
| 致谢 | 第66-67页 |
| 附录 攻读学位期间发表的学术论文目录 | 第67页 |