面向对象并发程序切片技术及其在程序验证中应用论文.pdf

苏州大学 硕士学位论文 面向对象并发程序切片技术及其在程序验证中的应用 姓名 何志学 申请学位级别 硕士 专业 计算机软件与理论 指导教师 张广泉 20080401 面向对象并发程序切片技术及其在程序验证中的应用中文摘要 中文摘要 程序切片是一种重要的程序分析技术 它通过提取程序中直接或间接影响某个特 定程序点变量值的语句达到分解程序的目的 随着对程序切片技术研究的深入 其应 用领域由软件调试 测试 软件维护扩展到逆向工程 再工程和程序验证等 面向对象技术仍是目前软件开发方法的主流 其中封装 继承 多态 并发等特 征都为程序的理解与分析提出了新的问题 本文针对面向对象程序的并发机制 介绍 了程序的图形化表示方法 面向对象并发系统依赖图 提出利用变量缓存表分析程 序语句间依赖关系的方法 根据分析结果构造面向对象并发系统依赖图 并在此基础 上采用改进的两步遍历图可达性算法计算动态切片 程序验证面临的主要问题是由于程序规模的增大 尤其是并发分量的增加 所带 来的状态空间爆炸问题 程序切片可以将程序中不影响待验证性质的语句删除以减小 针对该程序抽象出的模型的复杂性 从而缩减其对应的状态空间 在一定程度上缓解 状态空间爆炸问题 本文提出一种从待验证的线性时序逻辑 l t l 性质中提取出切 片准则对程序进行切片的方法 切片后的程序与原程序关于待验证的l t l 性质具有 相同的可满足性 而其对应的状态转换图中的状态个数明显减少 随着i n t e m e t 技术和w w w 技术的发展 w e b 应用涉及的范围越来越广 程序规 模在不断扩大 其复杂性也越来越高 针对j a v aw e b 开发中关键技术的实现机制 把程序切片技术引入到w e b 应用程序的分析中 定义了w e b 应用程序中存在的依赖 关系 提出了一种构造w r e b 程序系统依赖图并计算程序切片的方法 在以上工作的基础上 本文以j a v a 语言实现的典型并发程序为例对以上提出的 方法在实际开发中的应用进行了说明 分析 关键字 程序切片 面向对象并发程序 程序验证 w e b 应用 作者 何志学 指导老师 张广泉 a b s t r a c t p r o g r a ms l i c i n gi sap r o g r a ma n a l y s i st e c h n i q u ew h i c he x t r a c t st h ee l e m e n t so fa p r o g r a mr e l a t e dt oap a r t i c u l a rc o m p u t a t i o n ap r o g r a ms l i c ec o n s i s t so ft h ep a r t so r c o m p o n e n t so fap r o g r a mt h a t p o t e n t i a l l y a f f e c tt h ev a l u e sc o m p u t e da ts o m ep o i n t so f i n t e r e s t r e f e r r e dt oa sas l i c i n gc r i t e r i o n s l i c i n gh a sb e e nw i d e l yu s e di nt e s t i n ga n d d e b u g g i n g p r o g r a mc o m p r e h e n s i o n a n ds o f t w a r em a i n t e n a n c e e t c n o w w i t hi t s d e v e l o p m e n t t h ea r e ai se x t e n d e dt ot h er e e n g i n e e r i n g p r o g r a mv e r i f i c a t i o n e t c o b j e c t o r i e n t e dp r o g r a ms t y l ei sb e c o m i n gt h en o r m s l i c i n go b j e c t o r i e n t e dp r o g r a m s p r e s e n t sn e wc h a l l e n g e sw h i c ha r en o te n c o u n t e ri nt r a d i t i o n a lp r o g r a ms l i c i n g t o s l i c ea n o b j e c t o r i e n t e dp r o g r a m f e a t u r e ss u c ha se n c a p s u l a t i o n i n h e r i t a n c e p o l y m o r p h i s ma n d c o n c u r r e n c yn e e d e dt ob ec o n s i d e r e dc a r e f u l l y t h i sp a p e rp r e s e n t s an e wm e t h o dt o s l i c i n gc o n c u r r e n t j a v ap r o g r a m s w ei n t r o d u c ec o n c u r r e n to b j e c t o r i e n t e ds y s t e m d e p e n d e n c eg r a p h c o s d g a st h ei n t e r m e d i a t ep r o g r a mr e p r e s e n t a t i o n o u rm e t h o d a p p l i e sv a r i a b l ec a c h et a b l e v c t t oa n a l y z et h ed e p e n d e n c i e si np r o g r a m sa n dt h e nt o c o n s t r u c tc o s d go ft h eg i v e np r o g r a m b u td o e sn o tu s ea n yt r a c ef i l et os t o r et h e e x e c u t i o nh i s t o r y b a s e do nt h i sm o d e l w eu s et h et w o p a s ss l i c i n ga l g o r i t h mt oc o m p u t e a c c u r a t ed y n a m i cs l i c e so fac o n c u r r e n tj a v ap r o g r a m p r o g r a mv e r i f i c a t i o ni sa ni m p o r t a n tm e t h o di na s s u r i n gt h ec o r r e c t n e s sa n dr e l i a b i l i t y o fc o m p u t e rh a r d w a r ea n ds o f t w a r e o n eo ft h em a j o rp r o b l e m si ss p a c e e x p l o s i o ni nt h e a p p l i c a t i o no ft h i sm e t h o dt oc o n c u r r e n ts o f t w a r es y s t e m s s t a t es p a c eg r o w se x p o n e n t i a l l y i nt h en u m b e ro fc o n c u r r e n tc o m p o n e n t s i nf a c t i ti so f t e nt h ec a s et h a ts o m eo ft h e s t a t e m e n t so ft h ep r o g r a ma r ei r r e l e v a n tt ot h ev e r i f i e dp r o p e r t ya n dc a nb ed e l e t e d i nt h i s p a p e r w ep r e s e n ta na p p r o a c hf o rs l i c i n gc o n c u r r e n to b j e c t o r i e n t e dp r o g r a m st or e d u c e t h es t a t es p a c ei nt h ep r o c e s so fp r o g r a mv e r i f i c a t i o n t h es a t i s f a c t i o no ft h ev e r i f i e d p r o p e r t yi sg u a r a n t e e df o rb o t hp r o g r a m sb e f o r ea n d a f t e rs l i c i n g a n dt h en u m b e ro fs t a t e s i nt h es t a t et r a n s i t i o ng r a p hi sd e c r e a s e d w i t ht h ed e v e l o p m e n to fi n t e m e ta n dw w wt e c h n i q u e s w e ba p p l i c a t i o ni sw i d e l y u s e di nm a n ye b u s i n e s sa r e a s a tt h es a m et i m e t h ef a c tt h a tl a r g e ra n dc o m p l e xw e b l i c o n c u r r e n to b j e c t o r i e n t e dp r o g r a ms l i c i n ga n di t sa p p l i c a t i o ni np r o g r a mv e r i f i c a t i o n a b s t r a c t a p p l i c a t i o np r o g r a m sb e c o m ei n c r e a s i n g l yam a i n s t r e a m i sc h a l l e n g i n gt h ep r o c e s so f d e v e l o p m e n t w ep r o p o s eam e t h o df o rs l i c i n gw e ba p p l i c a t i o np r o g r a mt oa n a l y z ea n d u n d e r s t a n dt h eb e h a v i o r so ft h ep r o g r a m b a s e do na l lt h e s ew o r k s w eg i v es o m et y p i c a le x a m p l e st oi l l u s t r a t eh o wt oa p p l yt h e m e t h o di n t op r a c t i c et h r o u g hj a v ac o n c u r r e n tp r o g r a m s k e y w o r d s p r o g r a ms l i c i n g c o n c u r r e n to b j e c t o r i e n t e dp r o g r a m p r o g r a mv e r i f i c a t i o n w e b a p p l i c a t i o n i i i w r i t t e nb yh ez h i x u e s u p e r v i s e db yz h a n gg u a n g q u a n 图表索弓 面向对象并发程序切片技术及其在程序验证中的应用 图表索引 图2 1c f g 例子程序 8 图2 2c f g 示例 8 图2 3 例子程序的程序依赖图 1 0 图2 4 系统依赖图例子程序 1 1 图2 5 系统依赖图 1 1 图2 6 无定形切片例子程序 1 4 图2 7 无定形切片 1 4 图3 1 类例子程序 1 6 图3 2 类依赖图 1 6 图3 3 继承关系 17 图3 4 多态方法实现程序 1 7 图3 5 多态选择边 1 8 图3 6v c t 例子程序 2 3 图4 1 客户端和服务器端交互过程 3 2 图4 2 客户端j s p 页面程序 3 3 图4 3 服务器端s e r v l e t 程序 3 5 图4 4w e b 应用程序系统依赖图 3 6 图4 5k r i p k e 结构的有向图表示 3 8 图4 6 满足a l l t p e u t p 彳 卿酌缈的计算树 4 0 图4 7 两条s t u t t e r i n g 等价路径 4 3 图5 1 生产者一消费者问题j a v a 程序实现 4 6 图5 2 生产者一消费者程序的t d g 和c o s d g 4 9 图5 3 简化的生产者一消费者j a v a 程序 5 0 图5 4 简化生产者一消费者程序的并发系统依赖图 5 1 图5 5 切片前例子程序的状态转换图 5 2 图5 6 切片后例子程序的状态转换图 5 2 表3 1 例子程序的v c t 2 3 表5 1 生产者一消费者程序的v c t 4 7 i v 苏州大学学位论文独创 性声明及使用授权的声明 学位论文独创性声明 本人郑重声明 所提交的学位论文是本人在导师的指导下 独立进 行研究工作所取得的成果 除文中已经注明引用的内容外 本论文不含 其他个人或集体己经发表或撰写过的研究成果 也不含为获得苏州大学 或其它教育机构的学位证书而使用过的材料 对本文的研究作出重要贡 献的个人和集体 均已在文中以明确方式标明 本人承担本声明的法律 责任 研究生签名 珥麦霍 日 期 趔监垒迎 学位论文使用授权声明 苏州大学 中国科学技术信息研究所 国家图书馆 清华大学论文 合作部 中国社科院文献信息情报中心有权保留本人所送交学位论文的 复印件和电子文档 可以采用影印 缩印或其他复制手段保存论文 本 人电子文档的内容和纸质论文的内容相一致 除在保密期内的保密论文 外 允许论文被查阅和借阅 可以公布 包括刊登 论文的全部或部分 内容 论文的公布 包括刊登 授权苏州大学学位办办理 研究生签名 珥焘整 日 期 麴监 受 超 导师签名 日期 如础 华 协 面向对象并发程序切片技术及其在程序验证中的应用 第一章绪论 1 1 研究背景及意义 第一章绪论 程序切片是一种程序分析技术 其基本思想是通过提取程序中直接或问接影响某 一个特定程序点处变量值的语句 达到分解程序的目的 例如给定程序尸 语句s 和 该处的变量 尸的静态后向切片包含当程序执行到s 时 尸中所有直接或间接对变 量v 有影响的程序片段 其中勺 诊称为切片准则 现在程序的规模越来越大 复杂度日益增加 同时对软件的可靠性 安全性等高 可信性质的要求也越来越高 所以如何分析 理解程序的行为 保证软件的正确性 可靠性成为软件工程一个重要研究方向 程序切片正是这样一种程序分解技术 它通 过寻找程序内部的相关性 也就是语句之间的依赖性分析 分解程序 再通过对分解 后所得到的程序片段即程序切片的理解和分析从而达到对整个程序的理解和分析 程序切片技术的研究有着极其重要的理论和实际意义 理论上 极大地丰富了程 序分析 程序理解 程序维护的理论基础 实践上 在程序分析 理解 调试 测试 度量 信息抽取 程序变换 软件维护 软件逆向工程 软件再工程中得到了广泛应 用 本文主要研究了面向程序源代码的分析方法 它是程序分析与验证的一个重要组 成部分 其意义主要表现在三个方面 首先 程序源代码包含了软件的所有细节 从 而源代码级的分析能够准确地回答所关心的程序性质是否得到实现 满足 其次 软 件所关心的大量性质本身就是针对程序源代码的 例如 程序运行状态 多线程的互 锁等 从而只能在源代码级进行分析和验证 同时程序编码又是最容易引入错误的阶 段之一 因此源代码级的分析能够确实提高对软件具体运行状况的理解 最后 从目 前软件工程方法的应用现状来看 软件重要性质保证的主要矛盾尚处在软件代码层面 上 在软件开发中 开发者把大量的时间和精力花费在寻找软件错误的调试和测试中 而结果依然是不完全的 面向对象程序开发技术依然是目前软件开发技术的主流 如何验证正在开发的程 序是否满足某些性质以及如何理解 分析已有的代码 更好的利用遗产代码都是实现 面向对象程序复用中所关注的问题 这些方法对现实中的开发都能够提供很好的支 持 随着实际应用对并发软件需求的不断增加 并发程序的分析 理解 测试和维护 第一章绪论面向对象并发程序切片技术及其在程序验证中的应用 已引起人们的高度重视 其中并发程序的切片技术己成为一个重要的研究课题 由于 并发程序的不确定性 目前尚有很多难点有待解决 针对顺序程序的分析方法和工具 无法直接应用到并发程序中 如何提高切片的效率和精确度一直是并发程序要解决的 问题 1 2 国内外研究现状 程序切片的概念是由m a r kw e i s e 首次提出削 w e i s e r 声称一个切片与人们在调 试一个程序时所做的智力抽象相对应 程序切片由两类定义方式 1 w e i s e r 定义的 切片是一个可执行的程序 是通过从源程序中移去零条或多条语句来构造的 2 另 一种定义是由程序中语句和控制谓词组成的一个子集 这些语句和控制谓词直接或间 接影响在切片准则计算的变量的值 这类切片不必构成可执行的程序1 2 w e i s e r 在程 序控制流图的基础上建立了数据流方程 然后 通过求解数据流方程来获得相应的程 序切茂 在程序依赖图和系统依赖图可达性算法的基础上 h o r w i t z r e p s 和b i n k l e y 等 提出了利用系统依赖图 s y s t e md e p e n d e n c eg r a p h s d g 计算过程间程序切片的两 步遍历图可达性算法1 3 由于在使用调用位置的可传递的依赖流信息中包含被调用过 程的上下文环境 所以 该算法的计算精度要比以前的算法高 程序切片计算算法从 基于控制流图的数据流方程的方法发展到基于依赖图的图可达性方法 4 在面向对象并发程序切片方面 国内外已经进行了比较深入的研究 提出了一些 切片方法 其中k r i s h n a s w a m y 通过对传统的程序依赖图进行面向对象扩充获得对象 依赖图 5 l a r s o n 和h a r r o l d 提出了类依赖图 面向对象的语句切片和对象切片的概 念 利用s d g 切片面向对象的程序1 6 j c h e n g 通过直接扩展顺序切片技术首次对并 发程序的切片技术进行了研究 他通过添加表示并发和同步的边 将系统依赖图推广 为系统依赖网计算程序切片 7 k r i n k e 针对干涉依赖的非传递性问题进行了研究 提 出线程见证的概念 通过使切片满足线程见证的条件 提出一个较为精确的并发程序 切片算法 8 驯 n a n d a 在k r i n k e 的基础上提出迹见证的概念 进一步提高了并发程序 切片的精度 l 明 国内 徐宝文 陈振强等针对大型程序分析效率低 并发程序分析结 果不精确等技术难题 在并发程序切片 1 1 1 大型程序切片 1 2 j 面向对象程序切片 1 3 切片技术及其应用等领域进行了深入研究 提出了针对a d a 并发程序的依赖性分析 2 面向对象并发程序切片技术及其在程序验证中的应用 第一章绪论 方法 以及对象切片 类切片和类层次切片的概念和方法等 l 6 徐宝文 张迎周 等从程序的形式化语义的角度考察了程序切片技术 提出了模块单子切片方法i r h l s 李必信提出一种对传统系统依赖图进行面向对象扩充的方案 该方案通过把传统的系 统依赖图和类依赖子图 类层次子图相结合 从而构成了描述面向对象程序的面向对 象系统依赖图 1 9 刎 并采用一种基于程序切片的方法来度量j a v a 的耦合性问题洲 建立了抽象数据切片和类内切片的概念 然后基于这两种切片讨论了j a v a 语言中存 在的内聚问题1 2 2 赵建军把已有的依赖图扩展成系统依赖网 s y s t e md e p e n d e n c e n e t s d n 并用s d n 来描述面向对象并发程序 然后在s d n 的基础上采用传统的节点 可达性算法来计算程序的切片 2 3 针对并发j a v a 程序提出了一种静态切片方法 该 方法采用多线程依赖图 m u l t i t h r e a d sd e p e n d e n c eg r a p h m t d g 来描述并发j a v a 程序语句间的依赖关系 并通过在这类依赖图上采用图可达性算法来计算所需的静态 切片1 2 卅 同时还尝试把切片技术运用到分析软件体系结构以及面向方面程序等方面 2 5 2 6 1 随着程序开发技术的发展 根据实际应用的需要 程序切片技术也由计算静态 切片发展到动态切片 2 7 1 有条件切片 2 8 由可执行的程序切片发展到不可执行的程 序切片 由程序源代码切片发展到软件规约切片 由单一切片发展到无定形切片 2 9 削片 3 0 1 砍片 等 1 3 本文研究内容 面向对象并发程序切片中的关键问题是如何确定因线程执行顺序的不确定性所 引发的语句间的依赖关系 针对该问题本文提出了基于变量缓存表的分析方法 计算 程序的动态切片 程序切片的应用范围不断扩大 已经从最初的调试 测试扩展到软 件开发过程的各个方面 本文主要关注了其在程序验证和w e b 应用程序分析方面的 应用 在程序验证过程中 由于并发分量的增加 使得程序的状态空间呈指数级增长 程序切片技术可以分离关注点 在建立程序状态转换图之前 就可以把与待验证性质 无关的语句删除 从而在一定程度上减小程序的规模 降低针对该程序构造的模型的 复杂度 缩减程序对应的状态空间 i n t e r a c t 技术和w w w 技术的发展 使得w e b 应用非常广泛 由于w e b 应用程序交互性强 语句间的依赖关系更加复杂 所涉及 的程序不再局限于一种语言 把程序切片技术引入到w e b 应用程序分析过程中 对 其开发提供了新的支持方法 第一章绪论面向对象并发程序切片技术及其在程序验证中的应用 本文的研究内容主要包括以下几点 1 针对面向对象并发程序的实现机制 定义了其中存在的各种依赖关系 在 面向对象并发程序中 不仅存在顺序程序中的数据依赖和控制依赖 还存在程序中各 个线程之间由于同步和访问共享变量引起的同步依赖和通信依赖 通过分析语句间的 依赖关系 构造出面向对象并发系统依赖图 2 由于在基于图论的程序切片计算方法中 关键是如何分析程序中存在的依 赖关系 基于此 本文提出构造变量缓存表 通过记录变量的定义和使用信息来分析 程序语句间的依赖关系 当计算动态切片时 变量缓存表中记录了变量的最后定义和 使用位置 而不是程序的执行历史 这区别于其他的计算方法 3 为了缓解程序验证过程中面临的状态空间爆炸问题 提出根据线性时序逻 辑 m 性质提取相应的程序切片准则 计算切片 把与待验证性质无关语句删除 的方法 4 针对w e b 应用程序中各种关键技术的实现机制 定义了交互程序中语句间 的依赖关系 通过分析这些依赖关系 构造系统依赖图 计算程序切片 从而把程序 切片技术引入到w e b 应用程序的分析过程中 1 4 本文组织结构 本文共分6 章 是根据从基础概念到具体工作 从基本理论到具体应用的思路来 组织安排的 具体如下 第1 章绪论 主要介绍了课题的研究背景 意义及国内外的研究现状 并对本文 的主要工作给出了概要说明 第2 章程序切片技术及其相关概念 详细介绍了程序切片技术尤其是面向对象并 发程序切片的基本概念 理论基础和分析方法 以及程序切片的分类 第3 章基于变量缓存表的面阿对象并发程序技术 详细阐述了本文提出的一种面 向对象并发程序切片方法 首先介绍了一种面向对象并发程序的表示方法 面向对 象并发系统依赖图 c o n c u r r e n to b j e c t o r i e n t e ds y s t e md e p e n d e n c eg r a p h c o s d g 然后提出利用变量缓存表分析程序语句间存在的依赖关系的方法 根据分析结果构造 面向对象并发系统依赖图 并在此基础上采用改进的两步遍历图可达性算法计算程序 切片 4 面向对象并发程序切片技术及其在程序验证中的应用第一章绪论 第4 章程序切片技术在程序验证中的应用 首先介绍了程序切片的基础应用情 况 并介绍了如何在w e b 应用程序分析过程中应用程序切片技术 然后 详细介绍 了上一章中提出的切片方法在模型检测中的应用 通过对欲验证的l t l 性质的分析 提取出对应的切片准则 然后根据该准则对原程序计算切片 切片后的程序与原程序 对待验证的l t l 性质具有相同的可满足性 而其对应的状态转换图中的状态个数明 显减少 这就在一定程度上缓解了状态空间爆炸问题 第5 章应用实例分析 通过对以j a v a 语言实现的典型并发程序为例 说明了本 文工作在实际开发中的应用过程 其中第3 4 5 章是本文的主要研究工作 第6 章总结与展望 对本文的工作做了总结 并对下一步工作进行了展望 第二章程序切片技术及其相关概念 面向对象并发程序切片技术及其在程序验证中的应用 第二章程序切片技术及其相关概念 本章主要介绍与程序切片相关的一些基本概念 首先定义了控制流图 一般程序 中存在的数据依赖和控制依赖关系 这是分析程序依赖性的基础 然后定义了程序依 赖图 系统依赖图等程序的图形化表示方法 最后介绍了程序切片的分类 2 1 程序切片技术概述 在计算机软件发展的过程中 程序的规模逐渐变大 复杂度逐渐增加 这使得如 何保证软件的可靠性 正确性 安全性等问题成为关注焦点 在程序的调试过程中 人们发现 当一个大的程序被分解成一个个较小的程序片段以后 很容易被构造 理 解和维护 随着各种程序分析 分解和理解技术的发展 w e i s e r 提出了程序切片的概 念 1 1 程序切片是一种程序分析技术 它通过提取程序中直接或间接影响某个特定程 序点变量值的语句达到分解程序的目的 软件开发技术 开发语言不断发展 相应的程序切片也出现了针对这些技术和语 言的方法 计算切片的算法从基于数据流方程 基于信息流关系发展到基于程序依赖 图 切片结果由可执行切片发展到不可执行切片 切片的粒度从源代码级逐步发展到 软件规约级 切片的目标程序由顺序程序发展到面向对象程序 并发程序 各种形式 的切片相继出现 切片类型由最初的静态切片 动态切片发展到条件切片 无定形切 片 削片 砍片等 程序切片的应用范围也由开始的程序调试 测试 维护逐步扩展 到复杂性度量 软件安全 软件重用 逆向工程和再工程 程序验证等 3 2 3 4 1 2 2 程序切片基本概念 现在计算程序切片主要使用的方法是基于依赖图的遍历算法 该算法以欲分析程 序对应的程序依赖图为基础 通过遍历该图得到最后的切片结果 为此下面介绍与之 相关的一些基本概念 6 面向对象并发程序切片技术及其在程序验证中的应用第二章程序切片技术及其相关概念 2 2 1 控制流图 控制流图 c o n t r o lf l o wg r a p h c f g 是一种通用的顺序程序表示方法 它反映 了程序中语句以及模块之间的执行顺序和调用关系 定义2 1 控制流图 程序尸的控制流图是一个有向图 可以用四元组 表示 其中s 为图中节点的集合 程序中的每条语句都对应于控制流图上的一个 节点 e 为图中的边集 庐 勺l 也 s i s 2 e s 且语句s l 执行之后 s 2 可能成为下一条 执行语句 路竹表示程序的入口节点 s e x i t 表示程序的出口节点 如果一个程序有 多个返回语句 则可以在图中设置一个虚拟节点 将其作为所有返回语句的后继节点 从而保证控制流图的完整性 定义2 2 直接前驱和后继 在c f g 中 若勺l s 2 e e 那么称s l 是眈的直接前 驱 记作p r e s l s 9 相应的称3 2 是s l 的直接后继 语句s 的所有直接前驱的集合称 为s 的直接前驱集 并记作p r e d s s 的所有直接后继组成的集合称为j 的直接后继 集 记作s u c c s 定义2 3 可执行路径 设语句序列勺l 观 s n 记作p a t h p a t h 是一条可执行路 径 当且仅当p r e s i 8 i 1 对于户1 2 e e n 1 时均满足 定义2 4 前驱和后继 在c f g 中 若j l 8 2 之间存在一条可执行路径 且s l 3 2 则称s l 是s 2 的前驱 记为p r e s l 眈 反之 称j 2 是s l 的后继 记为s u e t 幸o l s 2 定义2 5 后必经节点 在c f g 中 在程序入口到程序出口的任意一条可执行路 径上 如果存在两个节点s l 3 2 每条经过j l 到程序出口的路径都要经过眈 那么称 眈是s l 的后必经节点 在图2 1 例子程序中实现了取得两个正整数中的较大者 其对应的c f g 如图2 2 所示 m 为程序的入v i 节点 即方法的头部 x i 为程序的出口节点 即方法的返 回语句 节点2 为节点3 的直接前驱 铒枷 2 3 4 9 s e x i t 为一条可执行路径 在该 路径上 节点2 是节点9 的前驱 节点9 是节点2 的后必经节点 而节点4 不是节点 2 的后必经节点 因为从节点2 到节点 x i t 同时存在 b t r v 2 3 7 9 i t 这样一条可 执行路径 7 第二章程序切片技术及其相关概念面向对象并发程序切片技术及其在程序验证中的应用 2 2 2 依赖关系 图2 1c f g 例子程序 图2 2c f g 示僻 程序切片技术的基础是依赖性分析 程序中语句间主要存在由访问变量引起的数 据依赖和由控制条件引起的控制依赖 设对于语句s 其定义集d e f s 扛lx 是语句s 处定义或改变的变量 引用集r e f s 缸lx 是语句s 处引用的变量 则设m 和刀为给定程序中两条不同的语句 如果有 一条从m 到 z 的执行路径 同时存在一个在m 处定义 刀处引用的变量 且该变量 在从m 到力的执行路径上的其他位置没有被重新定义 则称n 数据依赖于m 定义2 6 数据依赖 语句 2 数据依赖于语句m 记作m 与n 当且仅当 1 存在由m 到以的路径尸 s 1 研 s 2 驴刀 且存在一个变量v 满足 d e j m 1 n r e a n 面向对象并发程序切片技术及其在程序验证中的应用第二章程序切片技术及其相关概念 2 对于路径p 上的其他语句s 尸一劬 疗 v 诺d e f s 设m 与以为给定程序中两条不同的语句 如果从m 至少可以引出两条执行路径 其中一条导致刀的执行 而另一条可能导致 2 不执行 则称p 控制依赖于m 定义2 7 控制依赖 语句 控制依赖于语句所 记作m 与聆 当且仅当 1 存在由m 到1 的路径p s l 聊 s 2 岛邗 对于路径p 上的其他语句 s p 一 加 刀 刀是j 的后必经节点 2 力不是m 的后必经节点 在程序设计中 有三种主要的控制结构 分别为顺序结构 判断结构与循环结构 顺序结构的语句在执行过程中依次执行 而控制依赖主要是由于控制结构改变程序流 向所引起的 在分析控制依赖的过程中 可以将顺序结构的语句简单看成一个程序节 点而不予考虑 因此只考虑判断结构 循环结构等会影响程序流程的语句 除此之外 还有其他的一些原因会引起控制依赖 例如过程调用 异常处理等 2 2 3 程序依赖图与系统依赖图 为了分析程序语句间存在的依赖关系 需要对其进行抽象 本文采用基于图论的 图形化表示方法 对于含有单个方法的程序而言 可以用程序依赖图表示 对于实际 应用中具有多个过程的程序而言 可以用系统依赖图来表示 程序依赖图 p r o g r a md e p e n d e n c eg r a p h p d g 由控制流图 控制依赖图 c o n t r o l d e p e n d e n c eg r a p h c d g 和数据依赖图 d a t ed e p e n d e n c eg r a p h d d g 组成 其中 控制流图如定义2 1 所述 它描述了一个程序中的控制流 控制依赖图包含了程序中 的控制依赖关系 其中的语句节点表示程序中的语句 谓词节点表示程序中的循环或 分支条件 数据依赖图是一个程序中语句间的数据依赖关系的集合 3 5 1 定义2 8 控制依赖图 控制依赖图c d g 是一个有向图 c 其中节点集s 是程 序中所有语句对应的节点集合 如果有语句眈直接控制依赖于语句s l 也就是有 墨与是 则把边岛寸岛加入到边集c 中 定义2 9 数据依赖图 数据依赖图d d g 是一个有向图 sd 其中节点集s 是程 序中所有语句对应的节点集合 如果有语句娩数据依赖于语句j l 也就是有 墨 蔓b j 则把边墨寸s 加入到边集d 中 定义2 1 0 程序依赖图 程序依赖图p d g 是一个二元组岱 e g s 是对应语 9 第二章程序切片技术及其相关概念面向对象并发程序切片技术及其在程序验证中的应用 句的节点集合 边集e e l ue 2 u 工其中 e l is l 与j 2 为控制 依赖边 e 2 ls 与s 为数据依赖边 x 表示程序中的其他依赖关系 对于程序p 中的两个语句s l s 2 若有s l 与j 2 或者j l 丝专s 2 成立 则称8 1 直接依赖于眈 记作d e p s l s 2 根据以上性质 我们可以定义传递依赖关系如下 对于方法m 中的三个语句s l 鼢s 3 s 1 传递依赖于s 3 记为d e p s l s 3 当且 仅当下面两个条件之一成立 1 d e p s 1 s 3 2 了s 2 d e p s l s 2 ad e p s 2 s g 图2 3 是图2 1 中例子程序对应的p d g 其中控制依赖关系为 3 与4 3 堕专7 数据依赖关系为 2 丝专9 4 堂专9 7 鱼0 9 卜 c o n t r o ld e p e n d e n c e 一 d a t ad e p e n d e n c e 图2 3 例子程序的程序依赖图 在实际的应用中 一个程序往往有多个过程相互调用来实现其功能 h o r w i t s 等 人引入了系统依赖图 3 l s y s t e md e p e n d e n c eg r a p h s d g 的概念来表示具有多个过程 的程序依赖图 一个s d g 是由一组过程间控制依赖边和流控制依赖边连接起来的过 程依赖图 p r d g 组成 p r d g 类似于p d g 但它还包括表示由于调用而形成的调用语 句 参数传递 可传递流依赖的节点和边 一个调用语句用一个调用节点 c a l lv e a e x 表示 用四种参数表示参数传递 在调用处 用a c t u a li n 和a c t u a lo u t 表示实际输入 参数和输出参数 它们控制依赖于调用节点 在被调用过程中 用f o r m a li n 和 f o r m a lo u t 表示形式输入参数和输出参数 它们控制依赖于过程入口节点 可传递的依赖边 又称s u m m a r y 边 加到a c t u a li n 节点和a c t u a lo u t 节点之间来 表示由于调用过程而形成的可传递流依赖 如果在被调用过程中相应的f o r m a li n 节 点和f o r m a lo u t 节点之间存在一条控制路径 流边或s u m m a r y 边 则在a c t u a li n 和 1 0 面向对象并发程序切片技术及其在程序验证中的应用第二章程序切片技术及其相关概念 a c t u a lo u t 之间加入一条s u m m a r y 边 使用三种类型的边把过程依赖图 p r d g 连接起来形成s d g 1 调用边 c a l le d g e 在每个调用位置节点和相应的过程入v 1 节点之间加入 调用边 2 参数输入边 p a r a m e t e ri n 在调用位置的每个a c t u a li n 节点到被调用过 程相应的f o r m a li n 节点之间加入参数输入边 3 参数输出边 p a r a m e t e ro u t 从被调用过程的f o r m a lo u t 节点加一条边到 相应的调用位置的a c t u a lo u t 节点 例如对于图2 4 中的程序 其对应的系统依赖图如图2 5 所示 其中在语句3 处 调用了过程a v g 语句3 和语句5 之间加入调用依赖边 实参彳 b 与形参 j 之 间加入参数输入边 过程a v g 返回值 与输出语句间加入参数输出边 在语句7 中 变量j 依赖于自身和五所以a c t u a l i n a a c t u a l i nb 与a c t u a l o u t a 之间加入s u m m a r y 边 图2 4 系统依赖图例子程序 图2 5 系统依赖图 第二章程序切片技术及其相关概念 面向对象并发程序切片技术及其在程序验证中的应用 2 3 程序切片的分类 从程序切片概念的最初提出到现在 切片技术一直随着软件设计 开发方法和程 序设计语言的发展而不断发展 以下从两个不同的角度介绍程序切片的分类 按照切片过程中在程序依赖图中遍历方向的不同对其分类如下 1 后向切片 给定程序p 语句s 和该语句处的变量v 根据切片准贝t j s 诊计算p 的后向切片 切片后的程序包含当程序执行到s 时 p 中所有直接或间接对v 有影响的程序片段 也就是说切片结果集合中包含的是程序中所有能够影响变量在切片准则的值的语句 和控制谓词 2 前向切片 给定程序尸 语句j 和该语句处的变量v 根据切片准则勺 诊计算p 的前向切片 切片后的程序是被v 在s 的值影响的语句和控制谓词的集合 在程序分析和测试过程中 前向切片和后向切片的作用都不可忽视 例如 如果 对一个已经测试完成的程序进行简单的修改 我们一定要知道这次修改可能会带来哪 些副作用 也就是这次修改可能影响后面哪些语句和控制谓词 显然这是一个计算前 向切片的河题 而另一方面 如果我们在程序测试过程中发现了某个错误 我们一定 要知道谁制造了这个错误 也就是前面的哪条语句或哪个谓词产生了这个错误 并如 何传播到我们发现它的地方 这显然是一个计算后向切片的问题 以下如没有特别说 明 均指计算程序的后向切片 按照切片准则的不同对其分类如下 1 静态切片 静态切片是对程序的静态分析 它针对的是程序所有可能的执行路径 而不考虑 具体的输入 这时的切片准则为 诊 其中s 为欲计算切片程序中的某一条语句 v 为语句s 处定义或引用的某一变量 例如在图2 l 所示的例子程序中 如果切片准则为 则无论x y 输入 为何值 计算出的静态切片结果均为 1 2 3 4 7 9 静态程序切片是 由程序p 中能够影响变量v 在某个特定程序位置s 的值的所有 1 2 面向对象并发程序切片技术及其在程序验证中的应用第二章程序切片技术及其相关概念 语句和控制谓词组成的集合 它考虑了程序所有可能的输入 当然也就包含所有可 能的执行路径 然而 在程序的调试过程中 处理一次错误执行时 一般关心的只是 如何定位导致错误执行的原因所在地 因而我们感兴趣的只是在某个特定情况下 而 不是在所有可能的输入情况下 如何保持程序的行为 我们把与某个特定输入相关的 切片称为动态切片 2 动态切片 动态切片的概念最初是由k o r e l 和l a s k i 于1 9 8 8 年提出的 2 7 1 动态切片只考虑对 于某个具体输入情况下程序的实际执行路径 此时的切片准则为勺 1 i o i n 其 中j 为欲切片程序中的一条语句 v 为s 处定义或引用的变量 矗为程序中某一个输 入变量的具体值 如果精确到s 语句的某一次出现 则切片准则可扩展为勺 1 i o f n 胗其中n 代表在计算切片时考虑的是语句s 在程序执行过程中的第刀次出现 例如 在图2 1 中 对于动态切片准贝j j 其中4 和7 分别代表x 和j 的输入值 则切片后的程序为 1 2 3 7 9 而在计算切片准则 对应的静态切片时 切 片后的程序为 l 2 3 4 7 9 可以看出 与静态切片相比 动态切片减少了切片的 大小 因为动态切片只考虑某个特定输入而静态切片要考虑所有可能的输入 同时 计算动态切片 考虑的是具体的输入情况 计算得到的切片更加精确 3 条件切片 条件切片是静态切片和动态切片的折中 在计算静态切片时 不考虑程序的具体 输入 而在计算动态切片时 只考虑程序的某一次的具体输入 这两种方法可以看作 是程序分析的两个极端 条件切片是在计算程序切片时 考虑程序输入的一个范围 即在切片准则勺 i o i n 的基础上 给出每个参数输入值的一个范围 而不是像 动态切片中给出每个参数的具体值 这增大了切片在程序理解方面的适用范围 例如 在图2 1 中 当参数x y 输入值分别为 1 4 和 4 0 时 这时对于切片准贝j j 来说 计算其条件切片的结果为 1 2 3 7 9 4 无定形切片 与传统切片类似 无定形切片在简化源程序的同时 保持了与原程序语义的一致 性 而同时无定形切片并不局限于只对程序进行语句删除 它可以在不改变程序语义 的条件下 利用所有可以利用的简化转换方式对程序进行简化 使得语义更加清晰 第二章程序切片技术及其相关概念面向对象并发程序切片技术及其在程序验证中的应用 例如对于图2 6 中例子程序而言 计算切片准则 对应的切片时 我们可以把r 的值带入到计算表达式 从而得到图2 7 中的结果 2 4 本章小结 图2 6 无定形切片例子程序 图2 7 无