（计算机科学与技术专业论文）基于开放时态逻辑的面向方面程序形式化验证和模块推理研究.pdf

摘要 摘要 面向方面程序设计( a s p e c t o r i e n t e dp r o g r a m m i n g ，a o p ) 是一种新的程序方 法学，代表程序方法学的发展趋势。面向方面程序设计减少由于软件项目重建而 带来的代码重构，大大提高软件系统的模块化和可重用性。作为一种新的程序方 法学，面向方面程序设计的应用和研究发展十分迅速。 由于面向方面语言( a s p e c t o r i e n t e dl a n g u a g e ，a o l ) 的不知觉性和多量化 特点，面向方面程序设计更容易引起行为干扰问题，使得面向方面程序的程序验 证和模块推理比传统程序方法学复杂的多。当程序员实现若干个方面，必须确保 每个方面与基本系统不产生行为干扰问题；如果多个方面横切基本系统的同一个 切入点，还要确保多个方面之间不产生行为干扰问题，面向方面程序的程序验证 和模块推理困难严重影响面向方面应用的发展前景。 传统形式逻辑的语义模型与面向方面程序的非对称行为模型存在失配，使用 传统的形式逻辑进行面向方面程序的形式化验证和模块推理十分困难。本研究提 出一种具有非对称行为模型的新时态逻辑一一开放时态逻辑( o p e nt e m p o r a l l o g i c ，o t l ) ，基于开放时态逻辑可以有效的解决面向方面程序的形式化验证和 模块推理问题，本研究的主要工作与贡献包括： ( 1 ) 定义开放时态逻辑的语法和语义。开放时态逻辑引入新的路径算子，描述 系统的内部路径和外部路径；引入新的时态算子，描述一些系统状态在外部动作 影响下的某种不变性。开放时态逻辑的语义模型是具有非对称性行为模型的开放 系统，适合描述面向方面程序的非对称行为模型。 ( 2 ) 提出基于开放时态逻辑进行面向方面程序的形式化规约和验证。方面干扰 问题与并发程序的并发进程干扰问题既存在相似性，也存在差异，本研究参考并 发程序的规约和验证方法，引入可横切依赖条件约束执行过程中的可能方面横 切。本研究的程序规约包括三个条件：前置条件、可横切依赖条件和后置条件。 基于本研究的程序规约建立一个证明系统进行面向方面程序的形式化验证，并证 浙江大学博士学位论文 明证明系统的有效性。 ( 3 ) 提出面向方面程序的模块约束和模块推理方法。根据面向方面程序的行为 特点，研究面向方面程序的模块化内涵。与本研究的程序规约类似，本研究的模 块规约也由三个条件组成：前置条件、可横切依赖条件和后置条件。基于本研究 的模块规约定义不同类型的模块约束，支持面向方面程序的模块推理和模块组 合。本研究定义了四种模块约束：可横切不变性、非横切不变性、可横切正确性 和非横切正确性，不同的模块约束支持不同的模块可靠性需求。 ( 4 ) 提出四种横切范式。应用本研究的形式化验证和模块推理方法，解决横切 同一个切入点的一组方面的行为干扰问题。横切范式基于不同类型的方面模块约 束和组合约束，确保横切同一个切入点的一组方面彼此之间不产生行为干扰。本 研究定义四种类型的横切范式：横切不变性范式、非横切不变性范式、横切正确 性范式和非横切正确性范式。 关键词：面向方面程序设计，形式化规约，形式化验证，模块推理，时态逻辑 a b s t r a c t a b s t r a c t a o p ( a s p e c t o r i e n t e dp r o g r a m m i n g ) i san e wp a r a d i g m ，w h i c hr e p r e s e n t st h e p r o m i s i n gt r e n do fp r o g r a mp a r a d i g m a o pr e d u c e sc o d er e f a c t o r i n gd u et ot h e r e c o n s t r u c t i o no fs o f t w a r ep r o j e c t s ，a n di m p r o v e st h em o d u l a r i z a t i o na n dr e u s a b i l i t yo f s o f t w a r es y s t e m s a san e w p r o g r a mp a r a d i g m ，t h ea p p l i c a t i o na n dt h er e s e a r c ho f a s p e c t o r i e n t e dp r o g r a m m i n gg r o w sr a p i d l y o w i n gt ot h ec h a r a c t e r i s t i c so fq u a n t i f i c a t i o na n do b l i v i o u s n e s so fa s p e c t - o r i e n t e d l a n g u a g e ，i ti sm o r el i k e l yt oc a u s et h ep r o b l e m so fb e h a v i o r a li n t e r f e r e n c e ，a n d p r o g r a mv e r i f i c a t i o na n dm o d u l a rr e a s o n i n go fa s p e c t o r i e n t e dp r o g r a m sa r em o r e d i f f i c u l tt h a nt h a to ft r a d i t i o n a lp a r a d i g m s w h e nt h ep r o g r a m m e r si m p l e m e n ts o m e a s p e c t s ，t h ei n t e r f e r e n c eb e t w e e ne v e r ya s p e c ta n dt h eu n d e r l y i n gs y s t e ms h o u l db e t a k e ni n t oa c c o u n t f u r t h e r m o r e ，w h e ns e v e r a la s p e c t sa r ew o v e ni n t oas a m ep o i n t c u t ， p o s s i b l ed a n g e r o u si n t e r f e r e n c e sa m o n gd i f f e r e n ta s p e c t ss h o u l da l s ob et a k e ni n t o a c c o u n t t h ed i f f i c u l t yo fp r o g r a mv e r i f i c a t i o na n dm o d u l a r r e a s o n i n g o f a s p e c t - - o r i e n t e dp r o g r a m sh i g h l y b l o c k st h e d e v e l o p m e n t o f a s p e c t - - o r i e n t e d p r o g r a m m i n g o w i n gt om i s m a t c hb e t w e e nt h es e m a n t i cm o d e lo ft r a d i t i o n a lf o r m a ll o g i ca n d a s y m m e t r i c a lb e h a v i o ro fa s p e c t o r i e n t e dp r o g r a m s ，i ti sn o tf i tf o rt r a d i t i o n a lf o r m a l l o g i c t o v e r i f ya n dm o d u l a r r e a s o n a s p e c t o r i e n t e dp r o g r a m s e x t e n d e df r o m t r a d i t i o n a lt e m p o r a ll o g i c ，an e wt e m p o r a ll o g i cn a m e do p e nt e m p o r a ll o g i ci s p r o p o s e dt ov e r i f ya n dm o d u l a rr e a s o na b o u ta s p e c t o r i e n t e dp r o g r a m s t h eb e h a v i o r a l m o d e lo fo p e nt e m p o r a ll o g i ci s a s y m m e t r i c a la n do p e n t h em a j o rw o r ka n d c o n t r i b u t i o n sa r ea sf o l l o w s ： f i r s t ，w ed e f i n et h es y n t a xa n ds e m a n t i c so fo p e nt e m p o r a ll o g i c o p e n t e m p o r a ll o g i ci n t r o d u c e sn e wp a t ho p e r a t o r st os p e c i f yi n t e r n a lp a r t sa n de x t e r n a l p a r t s ，a n di n t r o d u c e so n en e wt e m p o r a lo p e r a t o rt oe n s u r es o m ei n v a r i a n t sd u r i n g s o m ee x t e r n a la c t i o n s t h eb e h a v i o r a lm o d e lo fo p e nt e m p o r a ll o g i ci sa no p e ns y s t e m ， w h i c hi sa s y m m e t r i c a la n do p e n ，a n di sf i tf o rs p e c i f y i n gt h eb e h a v i o r a lm o d e lo f 浙江大学博士学位论文 a s p e c t - o r i e n t e dp r o g r a m s s e c o n d ，w ep r o p o s et of o r m a l l ys p e c i f ya n dv e r i f ya s p e c t o r i e n t e dp r o g r a m s b a s e do no p e nt e m p o r a ll o g i c s i n c et h e r ee x i s tb o t hs i m i l a r i t ya n dd i f f e r e n c e b e t w e e na s p e c ti n t e r f e r e n c ea n dp r o c e s si n t e r f e r e n c eo fc o n c u r r e n tp r o g r a m s ，w e d e f i n ec r o s s c u t a b l er e l y c o n d i t i o nt oc o n s t r a i np o s s i b l ec r o s s c u t t i n gd u r i n gt h ep r o c e s s o fe x e c u t i o n ，w h i c hr e f e r e n c e df r o mt h em e t h o do fs p e c i f y i n ga n dv e r i f y i n gc o n c u r r e n t p r o g r a m s p r o g r a ms p e c i f i c a t i o no fo u rr e s e a r c hc o n s i s t so ft h r e ep a r t s ：p r e c o n d i t i o n ， e r o s s c u t a b l er e l y - c o n d i t i o na n dp o s t c o n d i t i o n w ee s t a b l i s hap r o o fs y s t e mt o f o r m a l l yv e r i f ya s p e c t o r i e n t e dp r o g r a m sb a s e do nt h ep r o g r a ms p e c i f i c a t i o n s t h e s o u n d n e s so ft h ep r o o fs y s t e mi sa l s op r o v e d t h i r d ，w ep r o p o s eam e t h o dt om o d u l a rc o n s t r a i na n dm o d u l a rr e a s o na b o u t a s p e c t - o r i e n t e dp r o g r a m s a c c o r d i n gt on e wc h a r a c t e r i s t i c s o fa s p e c t - o r i e n t e d p r o g r a m s ，w ed e f i n en e wm o d u l a r i z a t i o nm e a n i n go fa s p e c t - o r i e n t e dp r o g r a m s s i m i l a rt op r o g r a ms p e c i f i c a t i o n s ，m o d u l es p e c i f i c a t i o n sc o n s i s t so ft h r e ec o n d i t i o n s ： p r e - c o n d i t i o n ，c r o s s c u t a b l er e l y c o n d i t i o n a n dp o s t c o n d i t i o n d i f f e r e n tm o d u l a r c o n s t r a i n t sa r ed e f i n e db ym o d u l es p e c i f i c a t i o n st os u p p o r tm o d u l a rr e a s o n i n ga n d m o d u l a rc o m p o s i t i o no fa s p e c t - o r i e n t e dp r o g r a m s w ei n t r o d u c ef o u rm o d u l a r c o n s t r a i n t s ：c r o s s c u t a b l ei n v a r i a n t ，n o n - c r o s s c u t a b l ei n v a r i a n t ，c r o s s c u t a b l ec o r r e c ta n d n o n c r o s s c u t a b l ec o r r e c t d i f f e r e n tm o d u l a rc o n s t r a i n t ss u p p o r td i f f e r e n tm o d u l a r r e l i a b i l i t y f o u r t h ，w ep r o p o s ef o u rk i n d so fc r o s s c u t t i n gn o r m a lf o r m b a s e do nt h e m e t h o d so ff o r m a lv e r i f i c a t i o na n dm o d u l a rr e a s o n i n go ft h i sr e s e a r c h ，w es e t t l et h e b e h a v i o r a lp r o b l e m st h a td i f f e r e n ta s p e c t sw o v e nt oas a n l ep o i n t c u tw i l li n t e r f e r ew i t h e a c ho t h e r b a s e do nd i f f e r e n tm o d u l a rc o n s t r a i n t sa n dc o m p o s i t i o n a lc o n s t r a i n t so f a s p e c t s ，c r o s s c u t t i n gn o r m a lf o r m se n s u r et h a td i f f e r e n ta s p e c t sw o v e nt oas a m e p o i n t c u tw i l ln o ti n t e r f e r e 、析t he a c ho t h e r w ei n t r o d u c ef o u rk i n d so fc r o s s c u t t i n g n o r m a lf o r m ：c r o s s c u t t i n gi n v a r i a n tn o r m a lf o r m ，n o n - c r o s s c u t t i n gi n v a r i a n tn o r m a l f o r m ，c r o s s c u t t i n gc o r r e c tn o r m a lf o r ma n dn o n c r o s s c u t t i n gc o r r e c tn o r m a lf o r m k e y w o r d s ：a s p e c t o r i e n t e dp r o g r a m m i n g ，f o r m a ls p e c i f i c a t i o n ，f o r m a lv e r i f i c a t i o n ， m o d u l a rr e a s o n i n g ，t e m p o r a ll o g i c 浙江大学博士学位论文 图目录 图1 1t o m c a t 的日志关注点实现2 图1 2 本文的主要内容及其关系图1 0 图2 1 笛卡尔的主客观认知观1 2 图2 2d o o y e w e e r d 的认知观1 4 图2 3d o o y e w e e r d 的方面模型1 4 图2 4 增强性环绕通知和旁路性环绕通知1 9 图2 5 例子2 1 2 1 图3 1 一个开放时态逻辑例子3 0 图3 2 例子2 1 附加前置条件和后置条件3 4 图3 3 例子2 1 附加前置条件、可横切依赖条件和后置条件3 9 图4 1p l 的执行过程中发生未知横切代码p 横切5 5 图4 2p 2 的执行过程中发生横切代码p 横切5 5 图5 1 可横切不变性的增量模块组合7 0 图5 2 可横切正确性的增量模块组合7 4 图6 1 横切不变性范式示意图7 7 图6 2 非横切不变性范式示意图7 9 浙江大学研究生学位论文独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作及取得的 研究成果。除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发 表或撰写过的研究成果，也不包含为获得逝姿盘鲎或其他教育机构的学位或 证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文 中作了明确的说明并表示谢意。 学位论文作者签名：易；蠡 签字日期： 矽7 年月j 7 日 学位论文版权使用授权书 本学位论文作者完全了解逝姿盘鲎有权保留并向国家有关部门或机构 送交本论文的复印件和磁盘，允许论文被查阅和借阅。本人授权逝望盘堂可 以将学位论文的全部或部分内容编入有关数据库进行检索和传播，可以采用影 印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名：五 签字日期：砟6 日 刖写日 袭州 致谢 致谢 首先诚挚的感谢指导教师应晶教授，应老师悉心的教导使我得以一窥计算机 软件研究领域的深奥，不时的讨论并指点我正确的方向，使我在这些年中获益匪 浅，应老师对学问的严谨更是我学习的典范。 本论文的完成另外亦得感谢实验室指导教师吴明晖的大力帮助，因为有他的 指导和帮助，使得本论文能够更加完整和严谨。 三年多的日子里，实验室里的共同生活点滴，学术上的讨论、言不及义的闲 扯、让人又爱又怕的宵夜、赶项目的革命情感、因为睡太晚而遮遮掩掩闪进实验 室，感谢众位学长、学弟和学妹们的共同砥砺，他们的陪伴让三年的学习和研究 生活变得绚丽多彩。 感谢学长、学弟和学妹们不厌其烦的指出我研究和生活中的缺失，且总能在 我迷惘时为我解惑释疑，也感谢蒋涛同学的帮忙，恭喜我们一起顺利走过这三年 多的博士生活。实验室的其它学弟、学妹们当然也不能忘记，他们的帮忙及其搞 笑我铭感在心。 妻子屠颖在背后的默默支持更是我前进的动力，没有妻子的体谅和包容，相 信这三年多的博士生活将是很不一样的光景。 最后，谨以此文献给我挚爱的双亲。 吕嘉 2 0 0 9 年6 月求是园 第l 章绪论 第1 章绪论 面向方面程序设计【”1 建立在传统程序方法学的基础上，通过扩充传统程序方 法学的结构和概念，模块化软件系统的横切关注点( c r o s s c u t t i n gc o n c e m ) ，有效 支持软件开发中的关注点分离( s e p a r a t i o no f c o n c e r n s ，s o c ) 【4 栅。由于面向方面 语言的多量化( q u a n t i f i c a t i o n ) 和不知觉( o b l i v i o u s n e s s ) 【2 ，7 】特点，面向方面程序 设计违反传统程序方法学的模块化原则1 8 1 ，容易引起方面干扰问题，造成面向方 面程序的程序验证和模块推理困难。 1 1 研究背景 1 1 1 面向方面方法学的兴起 在软件开发方法中，一般将系统的主要问题分解成不同的子功能，目标是尽 量降低不同子功能之间的依赖程度，这一过程称为关注点分离，其中每一个关注 点对应系统一个子功能，系统功能被分解成不同的关注点。关注点分离有利于提 高软件系统的可理解性和有效性，传统的程序方法学使用过程调用和对象封装 来实现关注点分离。对于复杂的软件系统，总是存在一些功能模块正交应用系统 的主要分解9 1 ，这些关注点称为横切关注点，典型的横切关注点包括： 支持应用系统的可靠性需求，例如日志和跟踪； 支持应用系统的安全需求，例如认证和授权； 支持应用系统的正确性需求，例如应用程序的某些不变特性保证； 关于应用系统的性能需求，例如缓冲区、缓冲池和缓存管理； 应用系统的辅助功能，例如支付和税收。 由于横切关注点与主要关注点正交，如果采用传统程序方法学( 面向过程语 言和面向对象语言) 实现横切关注点，容易引起代码分散( c o d es c a t t e r i n g ) 和代 码混杂( c o d et a n g l i n g ) 问题，代码分散和代码混杂违反传统的程序模块化原则， 使得应用程序难以有效的维护和进化。例如w e b 服务器t o m c a t 里的日志功能实 现分散在系统的各个模块( 如图1 1 ) ，仅仅使用主流面向对象语言j a v a 很难模块 1 晰江大学博学位论文 化 霸 图i 】t o m c a t 的日志关注点实现 面向方面程序设计建立在传统程序方法学的基础上，通过扩充传统语言的结 构和概念模块化横切关注点，解决由于关注点分离引起的代码分散和代码混杂问 题，减少由于软件项目重建而带来的实现改动，面向方面程序设计大大提高复杂 系统的模块化和可重用性。随着面向方面语言和面向方面程序设计理论的发展， 越来越多的软件开发转向面向方面的软件开发( a s p e c t o r i e n t e ds o f t w a r e d e v e l o p m e n t ，a o s d ) 【1 们“，当前的面向方面应用主要包括： 大型软件系统的模块化，这一类应用系统一般功能比较复杂，例如电信 系统和医保系统； 给遗留系统附加功能，这些功能可能正交依赖系统的主要分解，例如附 加应用程序的日志、跟踪和认证功能； 面向方面的戟件产品线技术，使用面向方面特性可以更好的支持软件产 品线进化 1 2 1 ； 软件系统的性能改进，例如可以使用面向方面程序特性可以将一个顺序 执行的应用引入并行执行特性 1 9 ，2 0 。 相对于传统的软件开发方法，面向方面程序设计的优点主要在于( 2 1 】： 软件模块的责任更加清晰，面向方面的软件开发使得一个软件模块只负 责它的相应关注点： 一爨 ，旦 第l 章绪论 提高软件系统的模块化，面向方面程序设计使得不同关注点的实现相互 分离，有利于降低不同关注点之间的耦合度； 使得软件系统更容易进化，由于横切关注点对于核心关注点具有不知觉 性，随着需求的变化，不同关注点的实现可以相对独立变化； 推迟设计决定，有利于软件开发者推迟体系结构的设计决定，从而避免 软件体系结构设计不足或者过度； 更好的支持代码重用，由于面向方面语言的增量化特征，可以给基本系 统附加增量化的行为影响；不同方面实现的低耦合，更有利于软件系统 的不同子功能的代码重用。 1 1 2 方面干扰问题的阴影 随着面向方面方法学的兴起，越来越多的复杂软件系统包含面向方面的设计 和实现，开发者期望使用不同的方面封装系统的不同关注点，对于系统不同关注 点的交互行为分析，就显得特别重要。 面向方面语言在传统模块组合方式上引入方面编织机制，不同关注点的实现 可以多量化和不知觉的编织在一起，但是这种多量化和不知觉的编织容易引起方 面干扰问题1 2 2 - 2 4 1 ：由于不知觉性，方面引入的行为影响对于基本系统具有不可知 性，可能引起基本系统不可预料的变化；由于多量化，方面干扰问题可能被放大 和很难控制。当程序员实现若干个方面，必须保证方面与基本系统不产生行为干 扰问题，如果多个方面横切基本系统的同一个切入点，还要确保多个方面之间不 产生行为干扰问题。 方面干扰严重影响面向方面应用的发展前景，造成面向方面程序的验证和模 块推理困难。完全不知觉性( t o t a lo b l i v i o u s n e s s ) 曾被认为对于面向方面程序设 计具有关键性意义，最近一些研究者开始倾向于放弃完全不知觉，基于部分不知 觉性( p a r t i a lo b l i v i o u s n e s s ) 提出不同的方法和技术解决方面干扰问题，支持面向 方面程序的验证和模块推理。 一部分研究者强调尽量维持传统的程序模块化原则，通过约束和改进现有的 浙江大学博士学位论文 面向方面语言解决方面干扰问题：文章【2 5 。川通过加强或者改进基本系统的模块接 口支持模块的局部推理；文章【3 1 1 通过定义方面( 或者通知) 的非干扰条件来进行 程序行为的局部推理；文章【3 2 1 通过约束联结点模型( 甚至替换联结点模型) 支持 面向方面程序的形式化推理；文章 3 3 - 3 5 1 通过扩展( 建立) 新语言( 核心演算) 进 行面向方面程序的程序验证和模块推理研究；文章 3 6 - 3 8 1 基于非经典形式逻辑进行 面向方面程序的程序验证和模块推理研究。 一些研究者发现面向方面程序的方面干扰与并发程序的并发进程干扰存在 相似性：不同方面在基本系统的特定执行点获得执行控制，通过方面执行可以修 改基本系统的程序状态，方面执行完成后返回基本系统的中断执行点( 或者跳过 特定的语句) ，因此可以借鉴并发程序的形式化验证方法进行面向方面程序的形 式化验证和模块推理，文, 3 9 , 4 0 1 使用信赖保证方法【4 1 4 4 1 ；文章3 8 ，4 5 5 4 1 使用模型检 查 5 5 - 5 7 】方法进行面向方面程序的程序验证和模块推理。 还有一部分研究者通过其它技术解决面向方面程序的验证和模块推理问题： 文章【5 8 1 借助面向对象程序设计的行为子类型【5 啦】约束对方面和基本系统的行为 关系进行约束，从而支持面向方面程序的模块推理；文章 6 3 - 6 6 1 通过程序切片【6 7 - 6 9 技术检查面向方面程序的正确性；文章1 7 0 1 提出基于高层的特定领域语言来解决方 面干扰问题。 以上面向方面程序的验证和模块推理研究的主要问题在于：第一类研究为了 维护传统的程序模块化原则，往往限制现有的面向方面语言的能力，在某些应用 场景下有可能得不偿失；第二类研究强调面向方面程序的方面干扰与并发程序的 并发进程干扰的相似性，但是忽视方面干扰与并发进程干扰的差异性；第三类研 究缺乏有效的形式化基础，只能发现方面干扰而不能证明方面干扰不存在，很难 作为普适性的解决方案。 1 1 3 软件工程和形式化方法 软件危机( s o f t w a r ec r i s i s ) 【7 1 1 指计算机软件系统在开发和维护过程中所遇到 的一系列严重问题。1 9 6 8 年北大公约组织( n a t o ) 的计算机科学家在德国召开 4 第1 章绪论 的国际学术会议上第一次提出软件危机的概念，软件危机包括两个方面的问题： 一、如何更有效的开发软件，以满足不断增长、日趋复杂的需求；二、如何维护 数量不断膨胀的的软件产品。 软件危机的表现主要表现在以下几个方面：软件成本日益增长；开发进度难 以控制；软件质量差；软件维护困难。造成软件危机的原因是多方面的，但是根 本原因在于软件系统本身所具有的复杂性，软件的复杂性主要体现在：软件规模 的复杂性；结构的复杂性；环境的复杂性；应用领域的复杂性；交流的复杂性。 为了克服软件危机，人们从多个方面进行了探索，提出种种解决方案。这些方案 归纳起来分为两类：一、采用工程化的方法组织和管理软件开发；二、从理论上 探讨程序正确性和软件可靠性问题。前者导致了软件工程的出现和发展，后者推 动了对形式化方法的深入研究。 形式化方法( f o r m a lm e t h o d ) 的基本含义是借助数学方法来研究计算机科学 中的有关问题。将形式化方法用于软件开发的主要目的是保证软件系统的正确 性，形式化方法基于严格的数学化方法。形式化方法一般包括三个方面的活动： 形式化规约，形式化验证和形式化精化。形式化规约( f o r m a ls p e c i f i c a t i o n ) 是计 算机系统的一个数学描述，描述系统做什么，不做什么；形式化验证( f o r m a l v e r i f i c a t i o n ) 是使用数学方法的证明目标系统满足或者不满足特定的形式化规约 或者特性；形式化精化( f o r m a lr e f i n e m e n t ) 又称程序变换，是将自动推理和形式 化方法相结合而形成的一门新技术，它研究从抽象形式规约推演出具体的面向机 器的程序代码的全过程【7 2 】。 1 2 研究动机和研究意义 1 2 1 研究动机 方面干扰问题严重影响面向方面方法学的发展前景，许多研究者采用不同的 方法和技术解决面向方面程序的验证和模块推理问题，但是这些研究一般存在以 下特点或者问题： 缺乏有效的形式化描述，或者采用传统的形式逻辑，传统的形式逻辑与 浙江大学博士学位论文 面向方面程序的行为模型存在失配，使用传统形式逻辑进行面向方面程 序的验证和模块推理比较复杂和困难。 一般研究者仅仅研究方面对于基本系统的方面干扰；另外一部分研究者 注意到不同方面之间的方面干扰；还有一部分研究者同时注意到这两种 问题，但是采用不同的解决方案分开来处理。 不同面向方面应用程序的可靠性需求可能是不同的，即使在同一个面向 方面应用程序内部，可靠性需求也可能是不同的。传统的解决方案总是 针对特定类型的方面干扰问题，基于特定的前提性假设，解决特定的程 序可靠性问题。 面向方面语言的不知觉性破坏传统的程序模块化原则，一部分研究者试 图通过约束或者修改现有的面向方面语言来维护传统的程序模块化原 则，从而限制了现有的面向方面语言的能力。 总之，现有的解决方案无法有效全面的解决面向方面程序的形式化验证和模 块推理问题。 1 2 2 研究意义 面向方面方法学还处于发展过程中，面向方面方法学还不成熟，面向方面方 法学还不可能像面向对象方法学那样受到普遍应用，很多研究者认为它只是传统 方法学一次能力扩展，还不能称为一种真正的主流方法学。本研究也认为新的通 用程序方法学可能未必是目前的面向方面方法学，但是研究面向方面方法学对于 导向新的主流程序方法学具有启发作用，新的主流程序方法学必将与面向方面方 法学具有某种联系，或者具有某些面向方面语言的特征。 从程序方法学的研究历史看，任何一种程序方法学的发展和成熟都离不开程 序的形式化验证和模块推理方法，对于方面干扰问题，现有的形式逻辑的描述能 力相对不足，需要建立一种适合描述面向方面程序的行为模型的形式逻辑，这对 于扩展形式逻辑的描述和推理能力也是有意义的。 传统的程序模块化原则强调模块的封装性和信息隐藏，但是面向方面语言的 6 第1 章绪论 不知觉性破坏了这一点，这也是目前面向方面语言受到诟病的主要原因。本研究 认为，传统的模块化内涵可能存在某些问题，它可能过分强调了模块本身的封装 性，而忽视模块之间的组合能力。由于面向方面语言引入了新的模块组合机制一 一方面横切，大大改进和提升程序模块的组合能力，针对新的模块组合方式，需 要提出新的程序模块化内涵和模块推理方法。 1 3 研究内容 针对面向方面程序的验证和模块推理困难，本研究参考现有的面向方面程序 的验证和模块推理解决方案，同时结合我们已有的研究成果【6 6 , 7 3 ，以开放时态逻 辑为形式化基础，以面向方面程序的形式化验证和模块推理为核心内容，具体研 究内容涉及： ( 1 ) 建立开放时态逻辑。研究现有时态逻辑与面向方面程序的行为模型的失 配问题；对现有的时态逻辑进行扩展，引入新的路径算子和时态算子，定义开放 时态逻辑的语法；基于开放时态逻辑的语法，定义开放时态逻辑的语义模型一一 开放系统，开放系统具有非对称的行为模型。 ( 2 ) 基于开放时态逻辑的面向方面程序的形式化规约和验证研究。研究现有的 程序形式化规约和验证方法，重点是并发程序的形式化规约和验证方法；以开放 时态逻辑作为形式化基础，引入可横切依赖条件，定义面向方面程序的程序规约； 建立一个面向方面语言的核心语言，在此基础上建立一个证明系统支持面向方面 程序的形式化验证，并证明证明系统的有效性。 ( 3 ) 基于开放时态逻辑的面向方面程序模块推理研究。研究传统的程序模块化 内涵，针对面向方面语言的新特性，提出面向方面程序的模块化内涵；以开放时 态逻辑作为形式化基础，参考本研究的面向方面程序的程序规约，定义面向方面 程序的模块规约；基于模块的正确性和不变性概念，定义不同类型的模块约束， 支持面向方面程序的模块推理和模块组合。 ( 4 ) 横切范式的定义及其判定方法研究。针对一组方面横切同一个切入点的方 面干扰问题，提出横切范式理论进行解决，不同的横切范式针对不同类型可靠性 7 浙江大学博士学位论文 需求；应用本研究的形式化验证和模块推理方法，定义横切范式的判定方法。 1 3 1 研究基础 我们前面的研究 6 6 , 7 3 1 通过参考面向对象程序设计中的行为子类型( b e h a v i o r a l s u b t y p i n g ) 概念5 9 4 2 ，提出横切不变性概念解决方面干扰问题，这对于本研究定 义面向方面程序的程序规约和模块规约，以及定义不同类型的模块约束和横切范 式，进行面向方面程序的形式化验证和模块推理是有借鉴意义的。 研究【7 3 】提出一个横切契约( c r o s s c u t t i n gc o n t r a c t ) 演算系统和一组推理规则 支持面向方面程序的模块推理，并证明了推理规则的有效性，这对于本研究建立 一个证明系统支持面向方面程序的形式化验证，并证明其有效性是有借鉴意义 的。研刘删使用程序切片技术来分析和优化横切不变性检测算法，对于本研究寻 找横切范式的判定方法是有帮助的。 对于本研究的研究目标，我们已经积累了一些相关的研究成果和研究经验， 再结合现有的其它研究成果，本研究的研究目标是切实可行的。 1 3 2 创新和特色 本研究建立一个新的时态逻辑一一开放时态逻辑，时态逻辑通过引入新的时 态算子和路径算子，建立一个具有非对称行为的语义模型一一开放系统，而传统 时态逻辑的语义模型是具有对称行为模型的迁移系统，开放时态逻辑扩展了传统 时态逻辑的描述和推理能力，这种扩展适应了面向方面程序的非对称行为特点， 可以有效的支持面向方面程序的形式化验证和模块推理。 本研究的程序规约和模块规约都是三个条件，而传统的程序规约和模块规约 一般使用二个条件或者四个条件。相对于两个条件的程序规约和模块规约，引入 第三个条件( 可横切依赖条件) 参考了并发程序的形式化验证方法，可以约束基 本系统执行过程中的方面横切影响；相对于四个条件的程序规约和模块规约，由 于面向方面程序的方面横切行为是非对称的，使用第四个条件( 保证条件) 就显 得冗余了，而且反射的约束条件在构造上比较困难。 本研究以一个简单的顺序命令语言为基础，定义一个面向方面语言的核心语 第l 章绪论 言，由于核心语言的简洁性，同时忽略程序代码的并行执行，可以有效的减小证 明系统的规模，确保推理规则的简洁性，同时确保本研究提出的形式化验证和模 块推理方法更具有普适性。 针对面向方面语言的新特点，本研究提出了新的程序模块化内涵，本研究认 为模块组合能力与模块的封装性同样重要。 由于面向方面方法学还处于发展过程中，对于面向方面程序设计方法和设计 模式的研究还处理探索过程中，本研究提出的横切范式理论对于面向方面程序设 计方法和设计模式研究有很好的发展和启迪作用。 在程序验证和模块推理策略上，对于计算复杂度比较简单的情况，本研究采 用直接基于定义进行验证和推理的办法；对于计算复杂度比较大的情况，本研究 选择增量式的验证和推理方法，可以大大的降低计算复杂度。 1 3 3 研究约束 由于研究范围和文章篇幅限制，本研究作出如下约束： 本研究讨论的形式化验证和模块推理方法针对动态横切方式，对于静态 横切方式，本研究看作是对基本系统的重构； 本文选择d i j k s t r a 顺序命令语言进行面向方面扩展，作为本研究的核心 语言，本研究只讨论面向方面程序的顺序执行，不讨论面向方面程序的 并发执行； 为了避免讨论范围过分复杂化，本研究仅讨论行为增强性的横切代码， 不讨论行为旁路性的横切代码； 本研究主要讨论基于方法调用的联结点模型，其它联结点模型可以简单 从本研究进行扩展。 1 4 文章结构 本文共分7 章，其结构如图1 2 所示： 9 浙江大学博士学位论文 图1 2 本文的主要内容及其关系囹 第一章绪论，介绍本研究的研究背景、研究动机和主要内容。 第二章面向方面方法学研究，研究面向方面方法学的哲学基础；讨论面向 方面语言的主要特征和概念；分析面向方面程序设计的过程、特征和方面干扰问 题，并通过一个实例进行说明。 第三章开放时态逻辑和面向方面程序形式化规约，研究现有时态逻辑的语 法和语义模型；在计算树逻辑的基础上提出开放时态逻辑的语法和语义模型，o 基 于开放时态逻辑，提出面向方面程序的程序规约方法。 第四章基于开放时态逻辑的面向方面程序形式化验证，研究现有的程序验 证方法，重点是并发程序的形式化验证方法；定义一个面向方面的核心语言，基 于开放时态逻辑提出一个证明系统支持面向方面程序的形式化验证，并证明其有 效性。 第五章基于开放时态逻辑的面向方面程序模块推理，研究传统的程序模块 化内涵，针对现有的面向方面语言的特点，定义新的程序模块化内涵；针对不同 类型的模块可靠性需求，定义不同类型的模块约束，提出本研究的面向方面程序 的模块推理方法。 1 0 第1 章绪论 第六章横切范式，针对横切同一个切入点的一组方面的方面干扰问题，提 出使用横切范式的方法进行解决；分析不同类型方面组合需求，基于不同类型的 方面模块约束和组合约束，定义不同类型的横切范式进行解决；应用本研究的形 式化验证和模块推理方法，给出不同类型的横切范式的判定方法。 第七章总结及其展望，总结全文并提出将来的进一步工作。 浙江大学博士学位论文 第2 章面向方面方法学研究 面向