基于开放时态逻辑的面向方面程序形式化验证和模块推理研究
| 致谢 | 第1-6页 |
| 摘要 | 第6-8页 |
| Abstract | 第8-14页 |
| 第1章 绪论 | 第14-25页 |
| ·研究背景 | 第14-18页 |
| ·面向方面方法学的兴起 | 第14-16页 |
| ·方面干扰问题的阴影 | 第16-17页 |
| ·软件工程和形式化方法 | 第17-18页 |
| ·研究动机和研究意义 | 第18-20页 |
| ·研究动机 | 第18-19页 |
| ·研究意义 | 第19-20页 |
| ·研究内容 | 第20-22页 |
| ·研究基础 | 第21页 |
| ·创新和特色 | 第21-22页 |
| ·研究约束 | 第22页 |
| ·文章结构 | 第22-25页 |
| 第2章 面向方面方法学研究 | 第25-37页 |
| ·面向方面方法学的哲学基础 | 第25-27页 |
| ·传统程序方法学的主客观认知论 | 第25-26页 |
| ·康德的认识论 | 第26页 |
| ·Dooyeweerd的认知观和方面哲学 | 第26-27页 |
| ·面向方面语言研究 | 第27-30页 |
| ·基本概念和结构 | 第27-28页 |
| ·多量化和不知觉性 | 第28-29页 |
| ·Aspect J | 第29-30页 |
| ·面向方面程序设计研究 | 第30-36页 |
| ·设计过程 | 第30-31页 |
| ·程序行为的非对称性 | 第31-33页 |
| ·方面行为分类 | 第33页 |
| ·方面干扰例子 | 第33-36页 |
| ·本章小结 | 第36-37页 |
| 第3章 开放时态逻辑和面向方面程序形式化规约 | 第37-53页 |
| ·现有时态逻辑研究 | 第37-40页 |
| ·线性时态逻辑 | 第38页 |
| ·计算树逻辑 | 第38-40页 |
| ·现有时态逻辑分析 | 第40页 |
| ·开放时态逻辑 | 第40-45页 |
| ·开放时态逻辑语法 | 第41-43页 |
| ·开放时态逻辑的非对称行为模型 | 第43-45页 |
| ·现有程序规约研究 | 第45-49页 |
| ·Hoare三元组 | 第46-48页 |
| ·信赖条件和保证条件 | 第48-49页 |
| ·假设规约和保证规约 | 第49页 |
| ·基于开放时态逻辑的面向方面程序规约 | 第49-52页 |
| ·可横切依赖条件 | 第49-50页 |
| ·三条件的面向方面程序规约 | 第50-51页 |
| ·例子 | 第51-52页 |
| ·本章小结 | 第52-53页 |
| 第4章 基于开放时态逻辑的面向方面程序形式化验证 | 第53-74页 |
| ·现有程序验证方法研究 | 第53-60页 |
| ·模型检查 | 第54-55页 |
| ·程序证明 | 第55-56页 |
| ·顺序程序验证 | 第56-57页 |
| ·并发程序验证 | 第57-59页 |
| ·现有的面向方面程序验证方法 | 第59-60页 |
| ·基于Dijkstra顺序命令语言的核心语言 | 第60-63页 |
| ·核心语言语法 | 第60-61页 |
| ·核心语言操作语义 | 第61-63页 |
| ·核心语言计算模型 | 第63页 |
| ·基于核心语言的证明系统 | 第63-73页 |
| ·赋值公理 | 第64-65页 |
| ·蕴含规则 | 第65页 |
| ·顺序规则 | 第65-67页 |
| ·横切规则 | 第67-69页 |
| ·条件规则 | 第69-70页 |
| ·循环规则 | 第70-71页 |
| ·有效性证明 | 第71-73页 |
| ·本章小结 | 第73-74页 |
| 第5章 基于开放时态逻辑的面向方面程序模块推理 | 第74-89页 |
| ·程序模块化内涵研究 | 第74-76页 |
| ·传统程序方法学的模块化 | 第74-75页 |
| ·面向方面程序的模块化内涵 | 第75-76页 |
| ·基于开放时态逻辑的模块规约 | 第76-77页 |
| ·现有的面向方面程序模块推理研究 | 第77-80页 |
| ·无害通知 | 第77-78页 |
| ·现有的方面正确性概念 | 第78页 |
| ·行为子类型和契约式设计 | 第78-80页 |
| ·基于开放时态逻辑的面向方面程序模块推理 | 第80-88页 |
| ·可横切不变性 | 第80-83页 |
| ·非横切不变性 | 第83-84页 |
| ·可横切正确性 | 第84-87页 |
| ·非横切正确性 | 第87-88页 |
| ·本章小结 | 第88-89页 |
| 第6章 横切范式 | 第89-104页 |
| ·横切不变性范式 | 第89-92页 |
| ·问题提出 | 第89-90页 |
| ·直接判定方法 | 第90-92页 |
| ·非横切不变性范式 | 第92-94页 |
| ·问题提出 | 第92-93页 |
| ·直接判定方法 | 第93-94页 |
| ·横切正确性范式 | 第94-99页 |
| ·问题提出 | 第94-95页 |
| ·增量式判定方法 | 第95-99页 |
| ·非横切正确性范式 | 第99-103页 |
| ·问题提出 | 第99页 |
| ·增量式判定方法 | 第99-103页 |
| ·本章小结 | 第103-104页 |
| 第7章 总结及其展望 | 第104-107页 |
| ·研究工作总结 | 第104-105页 |
| ·未来工作展望 | 第105-107页 |
| 参考文献 | 第107-114页 |
| 攻读博士学位期间主要的研究成果 | 第114-115页 |
| 个人简介 | 第115页 |
