基于开放时态逻辑的面向方面程序形式化验证和模块推理研究

论文摘要

面向方面程序设计（Aspect-Oriented Programming,AOP）是一种新的程序方法学,代表程序方法学的发展趋势。面向方面程序设计减少由于软件项目重建而带来的代码重构,大大提高软件系统的模块化和可重用性。作为一种新的程序方法学,面向方面程序设计的应用和研究发展十分迅速。由于面向方面语言（Aspect-Oriented Language,AOL）的不知觉性和多量化特点,面向方面程序设计更容易引起行为干扰问题,使得面向方面程序的程序验证和模块推理比传统程序方法学复杂的多。当程序员实现若干个方面,必须确保每个方面与基本系统不产生行为干扰问题;如果多个方面横切基本系统的同一个切入点,还要确保多个方面之间不产生行为干扰问题,面向方面程序的程序验证和模块推理困难严重影响面向方面应用的发展前景。传统形式逻辑的语义模型与面向方面程序的非对称行为模型存在失配,使用传统的形式逻辑进行面向方面程序的形式化验证和模块推理十分困难。本研究提出一种具有非对称行为模型的新时态逻辑——开放时态逻辑（Open TemporalLogic,OTL）,基于开放时态逻辑可以有效的解决面向方面程序的形式化验证和模块推理问题,本研究的主要工作与贡献包括:（1）定义开放时态逻辑的语法和语义。开放时态逻辑引入新的路径算子,描述系统的内部路径和外部路径;引入新的时态算子,描述一些系统状态在外部动作影响下的某种不变性。开放时态逻辑的语义模型是具有非对称性行为模型的开放系统,适合描述面向方面程序的非对称行为模型。（2）提出基于开放时态逻辑进行面向方面程序的形式化规约和验证。方面干扰问题与并发程序的并发进程干扰问题既存在相似性,也存在差异,本研究参考并发程序的规约和验证方法,引入可横切依赖条件约束执行过程中的可能方面横切。本研究的程序规约包括三个条件:前置条件、可横切依赖条件和后置条件。基于本研究的程序规约建立一个证明系统进行面向方面程序的形式化验证,并证明证明系统的有效性。（3）提出面向方面程序的模块约束和模块推理方法。根据面向方面程序的行为特点,研究面向方面程序的模块化内涵。与本研究的程序规约类似,本研究的模块规约也由三个条件组成:前置条件、可横切依赖条件和后置条件。基于本研究的模块规约定义不同类型的模块约束,支持面向方面程序的模块推理和模块组合。本研究定义了四种模块约束:可横切不变性、非横切不变性、可横切正确性和非横切正确性,不同的模块约束支持不同的模块可靠性需求。（4）提出四种横切范式。应用本研究的形式化验证和模块推理方法,解决横切同一个切入点的一组方面的行为干扰问题。横切范式基于不同类型的方面模块约束和组合约束,确保横切同一个切入点的一组方面彼此之间不产生行为干扰。本研究定义四种类型的横切范式:横切不变性范式、非横切不变性范式、横切正确性范式和非横切正确性范式。

论文目录

• 致谢
• 摘要
• Abstract
• 第1章 绪论
• 1.1 研究背景
• 1.1.1 面向方面方法学的兴起
• 1.1.2 方面干扰问题的阴影
• 1.1.3 软件工程和形式化方法
• 1.2 研究动机和研究意义
• 1.2.1 研究动机
• 1.2.2 研究意义
• 1.3 研究内容
• 1.3.1 研究基础
• 1.3.2 创新和特色
• 1.3.3 研究约束
• 1.4 文章结构
• 第2章 面向方面方法学研究
• 2.1 面向方面方法学的哲学基础
• 2.1.1 传统程序方法学的主客观认知论
• 2.1.2 康德的认识论
• 2.1.3 Dooyeweerd的认知观和方面哲学
• 2.2 面向方面语言研究
• 2.2.1 基本概念和结构
• 2.2.2 多量化和不知觉性
• 2.2.3 Aspect J
• 2.3 面向方面程序设计研究
• 2.3.1 设计过程
• 2.3.2 程序行为的非对称性
• 2.3.3 方面行为分类
• 2.3.4 方面干扰例子
• 2.4 本章小结
• 第3章 开放时态逻辑和面向方面程序形式化规约
• 3.1 现有时态逻辑研究
• 3.1.1 线性时态逻辑
• 3.1.2 计算树逻辑
• 3.1.3 现有时态逻辑分析
• 3.2 开放时态逻辑
• 3.2.1 开放时态逻辑语法
• 3.2.2 开放时态逻辑的非对称行为模型
• 3.3 现有程序规约研究
• 3.3.1 Hoare三元组
• 3.3.2 信赖条件和保证条件
• 3.3.3 假设规约和保证规约
• 3.4 基于开放时态逻辑的面向方面程序规约
• 3.4.1 可横切依赖条件
• 3.4.2 三条件的面向方面程序规约
• 3.4.3 例子
• 3.5 本章小结
• 第4章 基于开放时态逻辑的面向方面程序形式化验证
• 4.1 现有程序验证方法研究
• 4.1.1 模型检查
• 4.1.2 程序证明
• 4.1.3 顺序程序验证
• 4.1.4 并发程序验证
• 4.1.5 现有的面向方面程序验证方法
• 4.2 基于Dijkstra顺序命令语言的核心语言
• 4.2.1 核心语言语法
• 4.2.2 核心语言操作语义
• 4.2.3 核心语言计算模型
• 4.3 基于核心语言的证明系统
• 4.3.1 赋值公理
• 4.3.2 蕴含规则
• 4.3.3 顺序规则
• 4.3.4 横切规则
• 4.3.5 条件规则
• 4.3.6 循环规则
• 4.3.7 有效性证明
• 4.4 本章小结
• 第5章 基于开放时态逻辑的面向方面程序模块推理
• 5.1 程序模块化内涵研究
• 5.1.1 传统程序方法学的模块化
• 5.1.2 面向方面程序的模块化内涵
• 5.2 基于开放时态逻辑的模块规约
• 5.3 现有的面向方面程序模块推理研究
• 5.3.1 无害通知
• 5.3.2 现有的方面正确性概念
• 5.3.3 行为子类型和契约式设计
• 5.4 基于开放时态逻辑的面向方面程序模块推理
• 5.4.1 可横切不变性
• 5.4.2 非横切不变性
• 5.4.3 可横切正确性
• 5.4.4 非横切正确性
• 5.5 本章小结
• 第6章 横切范式
• 6.1 横切不变性范式
• 6.1.1 问题提出
• 6.1.2 直接判定方法
• 6.2 非横切不变性范式
• 6.2.1 问题提出
• 6.2.2 直接判定方法
• 6.3 横切正确性范式
• 6.3.1 问题提出
• 6.3.2 增量式判定方法
• 6.4 非横切正确性范式
• 6.4.1 问题提出
• 6.4.2 增量式判定方法
• 6.5 本章小结
• 第7章 总结及其展望
• 7.1 研究工作总结
• 7.2 未来工作展望
• 参考文献
• 攻读博士学位期间主要的研究成果
• 个人简介