基于开放时态逻辑的面向方面程序形式化验证和模块推理研究
发布时间：2023-04-02 11:11
面向方面程序设计(Aspect-Oriented Programming,AOP)是一种新的程序方法学,代表程序方法学的发展趋势。面向方面程序设计减少由于软件项目重建而带来的代码重构,大大提高软件系统的模块化和可重用性。作为一种新的程序方法学,面向方面程序设计的应用和研究发展十分迅速。 由于面向方面语言(Aspect-Oriented Language,AOL)的不知觉性和多量化特点,面向方面程序设计更容易引起行为干扰问题,使得面向方面程序的程序验证和模块推理比传统程序方法学复杂的多。当程序员实现若干个方面,必须确保每个方面与基本系统不产生行为干扰问题;如果多个方面横切基本系统的同一个切入点,还要确保多个方面之间不产生行为干扰问题,面向方面程序的程序验证和模块推理困难严重影响面向方面应用的发展前景。 传统形式逻辑的语义模型与面向方面程序的非对称行为模型存在失配,使用传统的形式逻辑进行面向方面程序的形式化验证和模块推理十分困难。本研究提出一种具有非对称行为模型的新时态逻辑——开放时态逻辑(Open TemporalLogic,OTL),基于开放时态逻辑可以有效的解决面向方面程序的形式化验...
【文章页数】：115 页
【学位级别】：博士
【文章目录】：
致谢
摘要
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 未来工作展望
参考文献
攻读博士学位期间主要的研究成果
个人简介
本文编号：3779121
【文章页数】：115 页
【学位级别】：博士
【文章目录】：
致谢
摘要
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 未来工作展望
参考文献
攻读博士学位期间主要的研究成果
个人简介
本文编号：3779121
本文链接：https://www.wllwen.com/shekelunwen/ljx/3779121.html