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