（计算机软件与理论专业论文）基于模块单子语义的程序切片技术研究.pdf

摘要 程序切片是一种重要的程序分析理解方法，用于从源程序中抽取对程序中特定点上的特定变量有影响 的语句和谓词，组成新的程序( 称作切片) ，然后通过分析切片来分析源程序的行为。二十多年来，人们 对它进行了广泛而深入的研究，取得了许多研究成果，使得它在软件调试、测试、维护、度量、程序变换、 软件逆向工程与再工程等方面得到广泛应用，受到了广大软件研究和开发人员的高度重视。 论文主要工作包括：( 1 ) 将程序切片这类计算抽象成独立于具体语言的切片单子转换器，据此提出一 种新型的形式化程序切片方法一模块单子切片，相应切片算法将具有较强的可重用性和程序语言适应性； ( 2 ) 通过这种新型的形式化切片方法研究过程间程序和含指针程序的切片：( 3 ) 实现模块单子切片算法，开 发相应的模块单子切片器。 论文工作的主要成果表现在以下几个方面： 设计了一种切片单子转换器s 1 i c e t 。我们将程序切片这类计算抽象成独立于具体语言的实体：切片 单子转换器，以此来统一描述切片计算。s 1 i c e t 不仅提供了一种抽象化表示程序切片的能力，而且 还允许人们访问其低层语义的细节部分。切片单子转换器可与其它( 表示某种程序特性) 的单子 转换器或单子组合，并通过提升函数，驴与这些不同程序特性进行交互，从而可计算具有不同特性 的程序切片。 提出了模块单子切片概念，并给出了一种高精度的动态切片方法模块单子动态切片。它是一种 随着程序的执行同时计算动态切片的正向切片方法，无需记录程序执行历史，从而将追踪的信息 量减少到最低。我们还证明了该单子切片算法所得结果是精确的，即算法可捕获对应p d g 中可达 信息，且算法结果中不含多余的依赖信息。该算法的平均每个变量单子切片的时间复杂度是线性 的，空间复杂度与程序执行的长度无关。 此基础上提出了模块单子静态切片算法。它可直接在抽象语法结构上计算切片，无需显示地构造 诸如p d g 的中间结构。此外，切片单子转换器的模块化抽象机制使得单子切片算法具有很强的可 扩展性和重用性。 为求过程间程序切片，提出了基于回填待定标号的两阶段单子切片算法。该算法可求按值、结果、 值一结果调用的过程间程序切片，且可避免上下文调用问题。与基于s d g 两阶段扫描算法相比， 因其无需构造p d g 和s d g ，故可避免由于程序复杂、s d g 过于庞大而难以理解、实现时内存空 间紧张等问题。 通过将指向分析融入到已有的模块单子切片，提出了一种改进的单子切片方法以处理含指针的程 序。不同于将指向分析与切片计算分开的传统切片方法，改进的单子切片方法将程序正向切片思 想与数据流迭代分析相结合，可同时进行切片计算和指向分析，从而保证了较高的精度，而且比 一般的数据流迭代方法节省空间。此外，它还继承了原有单子切片方法所具有的强重用性和程序 语言适应性的优点。 开发了一个程序切片器原型系统，实现了我们的模块单子切片技术。我们所开发的切片系统s 基于模块单子语义，结合共代数和类属概念，支持增量式开发，其实现语言为h a s k e l l 。 关键词： 程序切片、单子、单子转换器、模块性、过程间、指针、h a s k e l l 、切片器 a b s t r a c t p r o g r a ms l i c m gl sa n1 m p o n a n tt e c l l l l l q u et oa 1 1 a l y z ea n du n d e r s t a n dp r o 伊a m s i ti su s e dt oe x 订a c tt h o s e s t a t e m e n t s ( a 1 1 dp r e d i c a t e s ) o fap r o g r a mt h a tm a yi n f l u e n c et h ev a r i a b l e sa tas p e c i a lp r o g 删i 】p o 破，a 1 1 dm a k e sa n e wp r o g r a m ( c a l l e das l i c e ) s ow ec a | 1 a 】1 a 】y z ea 1 1 du n d e r s t a i 】dt 1 1 e 厕百n a lp r o g r a m sb ya n a l y z j n gt 1 1 e i r c o r r e s p o n d m gs l l c e s o v e rt l l el a s tt w od e c a d e s ，m a n yr e s e a r c h e so np r o g m ms l i c i l l gh a v eb e e nd o n e ，a i l dl o t so f s l i c i l l gm e t l l o d sh a v eb e e np r e s e n t e d n o w p r o g r a ms l i c i n gh a sb e e nw i d e l yu s e di 1 1s o f h a r ed e b u g g i n t e s t i n 岛 m a i n t e n a n c e ，m e a s u r e m e n t ，r e v e r s ea i l dr e e n g i n e e r i n g t h em a i nr e s e a r c hi nt h i sp a p e ri n c l u d e s ：( 1 ) t h i sp a p e rp r e s e n t san o v e lf o m a lm e t h o df o rp r o g m m s l i c i n g ， t h em o d u l a rm o n a d i cs e m a n t i c s - b a s e ds l i c i n gt e c l l l l i q u e ，b ya b s t r a c t i n gt h ec o m p u t a t i o no fp r o g r a ms l i c i n ga sa 1 a n g u a g e i n d 印e n d 肌c eo b j e c t ，s l i c em o n a dt r a l l s f o n l l e r t h en e ws l i c i n gm e t h o dh a se x c e l l e n tr e u s a b i l i t ya i l d 1 a n g u a g e n e x i b i l i 妙p r o p e n i e s ( 2 ) t h ep a p e rg i v e st l l e 印p r o a c h e st oe x t e n do u rn e ws l i c i n gm e t l l o df o r h a l l d l i n g p r o c e d u r e sa n dp o i n t e r s ( 3 ) t h ep a p e ra l s oi m p l e m e n t so u rs l i c i n ga k 尹d 打t h m sa n dd e v e l o p e sam o n a d i cs i i c e r t h em a i nc o n t r i b u t i o n so ft 1 1 ep a p e ra r el i s t e da sf o l l o w s 。d e s i g i las l i c em o n a dt r a n s f - o n n e rs l i c e t w ea b s t r a c tt h ec o m p u t a t i o no fp r o 掣锄s l i c i l l ga sa 1 1i n d 印e n d e n t e n t i 吼s ，f c pm d 甩口d 打讼n i a ，7 竹p ，m r o u g hw h i c hd e s c r i b et h ef b a t u r e so fp r o g r a ms l i c i n g s l i c e tp r o v i d e st h e p o w e rn e e d e dt or e p r e s e n tt l l ea b s 仃a c tn o t i o no fp r o 伊锄s l i c i n g ，b u ts t i l la l l o w su st oa c c e s si t sl o w 1 e v e l s e m a l l t i cd e t a i l s t h eo p e r a t o r ，班i ns l i c e ta 1 1 0 w su st oc o n s i d e r 也ei n t e r a c t i o n sb e t w e e np r o 盯啪s l i c i l l g a n do t h e rc o m p u t a t i o nf e a t i l r e s b yc o m b i n i n gs l i c e tw i t ho t l l e rm o n a d s 仃a n s f o 肌e r so rm o n a d s w ec a n a 1 1 a l y z em o n a d i cs l i c i n gf o rp r o 擎a m sw i t hs p e c i a lc o m p u t a t i o nf e a t u r e s 。p r e s e n t6 r s tt 1 1 ec o n c e p to fm d 幽肠r 朋d 以口妣p ，- 0 矽伽咒s ，f c 扬g ，a n dg i v eah i g h l yp r e c i s ed y n 锄i cs l i c i n g m e t l l o d s m o d u l a rm o n a d i cd ”锄i cs l i c i n g i ti saf o r w a r dp r o 蓼锄s l i c i l l g ，c a i ld i r e c t l yc o m p u t es l i c e s o na b s 仃a c ts y n t a ) 【w i t l l o u tt h en e e d st or e c o r da 1 1e x e c u t i o nl l i s t o 够s ot l l em o n a d i cs l i c i n gr e d u c e st h e 仃a c i i l gi n f o 册a t i o nt oi t sm i l l i m u m w ep r o o ft 1 1 a tt l l em o n a d i cd y l l a l i l i cs l i c i l l gm e 廿1 0 di sp r e c j s e ，s i n c et 1 1 e a l g o r i t h l l lc a i lc 印t u r ea l l r e a c h a b l ei 1 1 f o 珊a t i o ni np d qa 1 1 dn os u p e r f l u o u sd 印e n d e n c ei n f o 肌a t i o nw i l lb e i n c l u d e di nt 1 1 es l i c i n gr e s u l t t h et i m ec o s to ft 1 1 em o n a d i cd y n a i i l i cs l i c ef o re a c hv a r i a b l e ，o n 廿1 ea v e r a g e ， i sl i n e a r - t h es p a c ec o s ti si r r e l a t e dt ot h el e n g t l lo fp r o g r a me x e c u t i o n 。p r e s e n tam o n a d i cs t a t i cs l j c i n ga 】g o m m ，w h j c hc a nc o m p u t es l i c e so na b s 白m c ts y l l t a xd i r e c 廿y ，谢d l o u tm e n e e d st oe x p l l c l t l yc o n s 仃u c ti i l t e n n e d l a t es m l c t u r e ss u c ha sc i e p e n d e n c e 鲫h s t h em o d u l a ra b s 勺r a c t i o n m e c h a l l i s m o fs l i c e ta l l o w s o u rm o n a d i c s l i c i n g m e t h o d p o s s e s se x c e l l e n tr e u s a b i l i t ya i l d 1 a n g u a g e n e x i b i l i t yp r o p e n i e s p r e s e n tb a c k f i l l i i l gi a b e l sb a s e dt w o - p h a s em o n a d i ca p p m a c ht oc o m p u t es t a t i cs i i c e so fap r 0 舀a mw i m c a l l - b y r e s u l t ，c a l l - b y v a l u e o r c a l l - b y v a l u e - r e s u l tp r o c e d u r e s c o r n p a r e dw i t l l t 1 1 es d g - b a s e d i n t e r p r o c e d u r a ls l i c i l l gm e t l l o d s ，o u rm o n a d i cm e m o dc a l la l s oa d d r e s sc a l l i i 培一c o n t e x tp r o b l e m ；o u rm e t l l o d c a l la v o i dt l l o s ep m b l e m sm a tt h es d gm a yb et o oc o n l p l i c a t et ob ea 1 1 a l y z e d ，i m p l e m e n t e da 1 1 du 1 1 d e r s t o o d f o ral a 唱e rp r o g m m ，s i l l c ew en e e d n tt oc o n s t l l j c ts d ga n dp d g 。b yi n 仃o d u c i i l gp o i n t - t oa j l a l y s i st om o u l a rm o n a d i cs l i c i n g ，w ep r e s e n ta na p p r o a c ht oe x t e n d 廿1 em o d u l a r m o n a d i cs l i c i l l gf o rh a n d l i i l gp o m e r s o u ra p p r o a c ho b t a i n st h ep o i n t t oi n f o 瑚a t i o nt i o u g ht h ed a t a f l o w i t e r a t i o n b e i n gd i a e r e n t 丘d mt l l et m d i t i o n a lm e t l l o d sw h e r et h ep o i i l t t oi n f o n n a t i o na n ds l i c i n ga r e a n a l y z e di nt w od i f r e r e n tp h a s e s ，t l l e ya r ec o m p u t e di nt 1 1 es a m ep h a s ei no u rm e t l l o d ，b yc o m b i n i n gt l l e f o n a r dm o n a ds l i c i n gw i t l ld a t a f l o wi t e r a t i o n i n s t e a do fr e c o r d i n g p o i l l t t oi n f o 册a t i o nf o re v e r v s t a t e m e n t ，w eo i l l yn e e dt or e c o r dm ei 1 1 f o 唧a t i o nf o rc u r r e n ta n a l y s i ss t a t e m e n t s s oo u rm e t h o ds a v e s s p a c ew i t h o u tl o s i n gt l l ep r e c i s i o n i na d d i t i o n ，o u r 印p r o a c ha l s o i n h e r i t st h ep r o p e r t i e so f1 a n g u a 2 e i n d e p e n d e n c ea n dr e u s a b i l i t ) ，丘o mt h eo r i g i n a lm o n a d i cs l i c i n gm e t h o d 。d e v e l o pap r o t o t y p es y s t e mo fp r o 伊a ms l i c e rf o rt h ei m p l e m e n t a t i o no fo l l rm o n a d i cs l i c i n g o u rm o n a d i c s l i c e rm p si sb a s e do nt 1 1 ei m e g m t i o no fi d e a s 丘o mm o d u l a rm o n a d i cs e m a l l t i c sa n dm ec o n c 印t so f c o a l g e b r aa n dg e n e r i cp r o 铲a i 【1 1 1 1 i n g i ti se m b e d d e di 1 1h a s k e l l ，a n ds u p p o n si n c r e m e n t a ld e v e l o p m e n t k e y w o r d s ：p r o g r a ms l i c i n g ，m o n a d ，m o n a d 仃a n s f o 舯e r ，m o d u l 撕t ) r ，i n t e 印m c e d u r a l ，p o i n t e r ，h a s k e l l ，s l i c e r i i 主要符号、术语列表 下面列出本文使用的主要术语和符号清单，其中斜体标注的为我们首次提出或使用的术语和符号。 q 朋p ，俐：历：莓直接堀用程序p 的唐堀程廖集3 1 c d m p 晰：语义枸趟欲手的最终单子1 0 c u n y 化5 0 d e “s ) ：定义集2 9 d 印：形参问纯款关秦3 2 e n v t ：环境单子转换器8 e 胛： 错误获取单子转换器一8 f i x ：不动点算子1 0 g s ：程序依赖图g 关于节点s 的切片1 1 g e t p t 、s e t p t 、l b p t 、u p d p t 昶m r g p t ： 指向集p t 的五个基本操作娩 g e 僦，j p 姗：妣e 丁手j 的滨取和勰终1 4 i n p u t ：动态切片时用户所关心的某个输入集一1 7 1 0 t ： i o 单子转换器一8 1 e 标号为l 的表达式e 1 0 上j 迸7 殆剪署句劳算历需袤迭式的衍号集合一1 4 三c ；堀钶篇处伤例标号集3 2 l i r ：单子转换器中的提升函数8 助砌1 ，：环境域e n v 中查找操作1 0 坳册、岫删f 和m 删f ? 臌田f c 船嘶操结1 4 p d g ： 程序依赖图1 l p 丁； 者廊集裁据结构4 2 砒口6 e 瓜，切三口6 p b ：研f c e 丁乒参辫三的蘑改移是新操结1 4 r e f ( s ) ：引用集一2 9 r e f ( s ，x ) ： 变量引用集2 9 r e f s ( 1 e ) ：加标表达式1 e 的变量引用集一1 7 陀m m ，6 觑d ：单子中两个基本函数6 s d g ： 系统依赖图2 6 彤记舀； 勿片麦数理结构_ 1 4 s t a t e t ： 状态单子转换器8 s u m m a 】了边2 6 印以向助：近凰最终勿片的秽篱璐西裁1 7 t c a l l ：施调程序中调用点处单子切片表一3 0 劢? 子程廖的最终勿序麦3 l 印c 口盯：倚对锯家巨新厅厅弹子_ 勿! 芹袤3 2 印m c ：兹堀搓绔最终点勉掌子勿手蓑2 9 印搬d ：存储域l o c 的更新操作1 0 形著言9 v 另u 名3 9 别名对表示法3 9 别名分析3 9 参数化语义7 程序切片一1 1 单子6 单子转换器8 定义次序依赖1 1 惰性计算4 9 后向切片1 1 可能别名3 9 可能数据依赖4 0 控制依赖一1 1 列表包含：5 1 流敏感指针分析3 9 流依赖1 1 模块单子语义9 模块性7 模式匹配一5 0 平凡计算6 前向切片一1 1 强更新一4 3 切片标准一1 1 勿片掌子肋c 以幻九耐1 4 勿片掌子转搀器肼c p 丁上n 1 4 确定别名一3 9 弱更新4 3 上下文敏感指针分析：4 0 正向切片2 指彩r 6 指向表示法：3 9 指向分析3 9 左值表达式4 0 一 论文插图、表格、主要算法列表 图2 1 算术表达式的一种参数化语义7 图2 2 一些常见的单子转换器8 图2 3 实例语言w 的抽象语法9 图2 4 实例语言w 的语义构造块1 0 图2 5 一个简单程序及其p d g 1 2 图3 1切片单子转换器s l i c e t 1 4 图3 2 跏甩( s ，三) 的定义1 7 图3 3实例语言w 的动态单子切片语义1 8 图3 4 一个w 源程序及其变量s 的动态切片一1 9 图3 5图3 4 ( a ) 程序的1 e 和尺咖( 1 e ) 1 9 图3 6图3 4 ( a ) 程序关于( a = 0 ，n = 2 ) 执行中的切片表s 1 i c e s 2 0 图3 7 实例语言w 的静态单子切片语义2 2 图3 8 一个实例程序2 l 图4 1 一个过程间实例程序2 7 图4 2图4 1 程序的s d g 2 7 图4 3以按值调用过程扩展w 语言的单子语义3 0 图4 4以按值结果调用过程扩展w 语言的单子语义3 l 图4 5 含一般过程的w 扩展语言的单子语义3 5 图4 6图4 1 程序的调用图及偏序关系3 6 图4 7 算法第一阶段所得的图4 1 中各个程序的单子切片结果3 7 图4 8图4 1 程序调用点处切片表t c a l l 、形参依赖集d 印和施调集c a l l e r 3 7 图4 9 算法第二阶段所得的图4 1 中各个程序最终单子切片结果3 8 图5 1 一个含指针的实例程序4 7 图6 1m s 的总体框架6 1 图6 2m p s 目前版本的用户交互界面6 1 图6 3m p s 对图3 8 程序进行动静态切片的结果6 3 图6 4m p s 对图3 4 ( a ) 程序进行动态切片的结果6 4 图6 5 一个w 循环程序的s 静态分析结果6 5 图6 6由表6 1 中数据生成的关系图6 6 表4 1图4 1 程序调用点处的临时标号集三c 3 6 表5 1与赋值语句相关的两种左值表达式的处理4 3 表5 2 与赋值语句相关的四种右值表达式的处理4 3 表5 3图5 1 程序的最终切片和指向集结果4 7 表6 1多层循环嵌套程序的单子静态切片结果比较6 6 算法3 1 模块单子动态切片算法1 7 算法3 2 模块单子静态切片算法2 1 i 东南大学学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。 尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过 的研究成果，也不包含为获得东南大学或其它教育机构的学位或证书而使用过的材料。与我 一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。 研究生签名：氆迎i 虱日期 锄s 4 f 6 东南大学学位论文使用授权声明 东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复印 件和电子文档，可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内容和纸质 论文的内容相一致。除在保密期内的保密论文外，允许论文被查阅和借阅，可以公布( 包括 刊登) 论文的全部或部分内容。论文的公布( 包括刊登) 授权东南大学研究生院办理。 研究生签名：1 垦堕囹导师签名：期：2 1 生生笪 ”- 一 第一章引言 1 1 选题依据 第一章引言 随着计算机技术的飞速发展，软件系统的数量越来越多，规模越来越大，复杂程度越来越高。在一些 大型、长生命周期的软件测试和维护过程中，手工分析已经变得越来越不可行，越来越多的工作需要理论、 技术与工具的支持。程序分析技术已成为软件领域的一个十分重要而又极其迫切的研究领域。 程序切片是由m w d s e r 提出的一种重要的程序分析理解方法【1 2 | 。给定程序p 、程序点p 和变量集v ， 其切片包含当程序执行到p 时，p 中所有直接或间接对v 中变量有影响的程序片断。其中， 称作切 片标准。程序切片分为两种：动态切片和静态切片。静态切片考虑程序所有可能的执行情况，与其输入无 关；动态切片只分析程序动态执行时所经过路径上的语句，随不同的输入而发生变化。程序切片技术已在 实际中得到广泛应用，所涉及的领域包括：程序分析、理解、调试、测试、软件维护、度量、逆向工程、 再工程等【3 16 】。 目前人们已提出了多种程序切片方法，常用的主要有：基于数据流方程的算法【2 和基于程序依赖图的 图可达性算法【l7 1 。此外，还有一些针对不同应用的扩充算法。但是，目前程序切片的算法还比较单一，基 本上还是采用基于依赖图的图可达性算法【l2 | 。现有的切片方法是顺序增量式的，非组合式的，从而模块性 较差。然而，现代的程序设计语言如a d a 、c + + 、j a v a 等都支持模块化的程序设计方法，即程序设计是组 合式的，程序可有几个模块组合而成。因此相应的程序分析方法( 包括程序切片) 应能反映该模块化设计 特性。 动态切片据特定的输入来分析程序执行中的依赖关系，因其结果小且精确，在程序调试、错误定位等 方面有着较高的应用价值。困扰动态切片应用的一个主要因素是目前方法的追踪效率较低【i8 1 。动态切片的 难点在于运行时信息的获取。为此，多数动态切片方法借助于关系图( 如控制流图、依赖图等) ，并追踪 程序的执行过程，故不可避免地需要相当大内存空间来记录执行历史。于是，动态切片技术研究的重点是 如何减少追踪的信息量。 j c h w a n 2 等人曾指出程序切片受该程序语言的语义特性影响，并证明了任一切片程序都不可能应用 到所有程序语言中【1 9 】，即程序切片算法是语言相关的，所以切片算法应具有较强的灵活性来适应所给定语 言的语义。另一方面，既然程序的行为是由其语义决定的，所以从形式化语义角度来研究程序切片是合理 的。目前基于程序语义的切片方法主要是基于传统指称语义的程序切片，即指称切片【2 0 2 2 】( 如n d 胁f i d ，z 口， s 比加前。但由于传统指称语义缺乏模块性和重用性【z 3 。2 5 】，所以指称切片方法很难扩展应用到包含更多程序 特性( 如过程、指针等) 的实际语言中。 本文在广泛调研的基础上，根据中兴、华为、7 1 6 所等民用和军工企事业研究单位的实际需求，结合 国家杰出青年科学基金项目( 6 0 4 2 5 2 0 6 ) 、国家自然科学基金( 9 0 4 1 2 0 0 3 ) 、教育部博士点基金( 2 0 0 2 0 2 8 6 0 0 4 ) 、 国家重点基础研究发展规划9 7 3 资助项目( 2 0 0 2 c b 3 1 2 0 0 0 ) 、国家自然科学基金青年科学基金( 6 0 3 0 3 0 2 4 ， 6 0 4 0 3 0 1 6 ) 、江苏省计算机信息处理技术重点实验室开放基金( 苏州大学) 、武汉大学软件工程国家重点实验 室开放基金，旨在研究一种新型的形式化程序切片方法基于模块单子语义的程序切片；通过深入研究 模块单子切片理论，直接在抽象语法项上计算单子切片，相应切片器中无需构造诸如控制流图或依赖图的 中间结构；在计算动态切片时也不必记录程序执行历史，提高了切片的效率和精度：通过将模块单子切片 技术应用到过程间和指针切片中，进一步说明我们的单子切片算法具有较强的可扩展性和重用性：研究和 开发模块单子切片系统，并作一些相应的试验结果分析。 东南大学博士学位论文 1 2 国内外研究现状 目前的大部分程序切片方法是基于数据流方程的算法和基于程序依赖图的图的可达性算法。正如前面 所述，这些方法缺乏模块性和语言适应性。本文将从另一个角度( 即程序的形式化语义) 来考察程序切片 技术。事实上，既然程序的行为是由其语义决定的，所以从形式化语义角度来研究程序切片是合理的。 1 1 语义切片技术 基于程序语义的切片方法源于1 9 8 9 年p a h a u s e r 发表的论文“d e n o t a t i o n a lp r o g r 锄s l i c i i l g ”。文中， 他利用程序指称语义的思想给出了一简单语言的指称切片器：通过函数6 记录某切片需要的所有相关变量， 此基础上再利用函数q 构建最终的静态切片。随后l o u a r b y a 等人扩展了该指称切片器使之能求过程间的 静态切片【2 l 】。g a v e l l l ( a t e s h 也注意到了指称语义在程序切片中的应用，在其1 9 9 1 年a c m 会议论文“t h e s e m a n t i ca p p m a c ht op r o g r a ms l i c i n g ” 2 2 】中给出了程序切片的形式化定义及其算法的指称描述。他所选用的 语言是个非常简单的程序语言，仅包含赋值、分支、循环和复合语句。但因受传统指称语义弱模块性限制， 该方法很难扩展应用到包含过程、指针等特性的实际语言中。 传统指称语义缺乏模块性和重用性已为人们所熟知，参见文献 2 3 ，2 4 ，2 6 ，2 7 。m o g g i 通过使用单子来 加强语义描述的模块性，单子将诸如状态、环境、异常和不确定性的程序“混杂”特性封装起来，仅允许 由单子所提供的一些操作来访问它们 2 8 1 。p j w a d l e r 将单子思想广泛应用于函数式程序设计领域【2 9 州】。但是， 在单子语义中无法将两个单子结合成一个新单子，为此，d e s p i n o s a 重新提出了m o g g i 早期报告中的单子构 造器概念，并重命名为单子转换器，它将给定单子转换成新单子，并增加新操作运算【32 1 。此基础上，s “a n g 等人提出了模块单子语义，使用单子和单子转换器描述程序语义，将程序基本概念( 如存储、环境等) 独立 地封装在单子转换器里【2 l3 3 ，j 。本文利用这强模块化的模块单子语义，研究一种新的语义切片方法。 2 1 动态切片技术 与静态切片相比，动态切片的精确度比较高，但由于动态切片需要追踪程序的执行，其执行代价较高， 因此需要在不降低精确度的情况下减小其代价。为此，多数动态切片方法借助于关系图( 如控制流图、依 赖图等) 来追踪程序的执行过程，故不可避免地需要相当大的内存空间来记录执行历史。因此，动态切片 技术研究的重点是如何减少追踪的信息量。 研究者们已提出了多种动态切片方法，见文献 8 ，1 5 ，1 8 ，3 5 3 9 。这些方法可分为两类：正向和逆向动 态切片。所谓正向切片是指在进行切片分析时，沿着程序执行流进行分析，而逆向切片正好相反。一般地， 逆向切片的基本思想是：在程序执行前分析源程序获得程序依赖图( p d g ) ，然后在程序执行过程中标记 p d g 中所执行过的节点或边，最后通过遍历p d g 得到程序的动态切片。 在b k o r e l 等提出的正向切片中，将所有语句分成若干可移动的块，当某个块执行完后由相应算法确 定该块是否被包括到切片中【36 | 。这样，在执行完最后一条语句的同时，得到了所有语句可执行的动态切片。 y s o n g 等将此方法推广到含结构化跳转语句的程序中【引，而g t i b o r 用它计算相关切片p7 1 。该正向切片方 法无需记录程序执行历史，但它不能计算潜在的依赖，使得结果不太精确。为此，陈振强在其博士学位论 文中，结合该正向切片方法和基于静态依赖图的标记节点方法，提出基于依赖性分析的动态切片方法【l 5 1 。 该方法提高了切片的精确度，但同时仍需要追踪程序执行过程。 3 ) 过程间程序切片技术 当前过程间程序切片技术主要是h o n i t z 等人【4 0 】所提出的基于系统依赖图( s d g ) 切片方法，它是一 种两阶段图的可达性算法。该算法很好地解决了调用上下文的问题，但存在由于程序复杂使得s d g 过于 庞大而难以理解、实现时内存空间紧张等问题。虽然研究者对该算法做了不少改进，但算法的性能并无本 质上的提高。 4 ) 含指针程序切片技术 指针的出现将导致别名问题4 1 ，4 2 1 ( 即多个变量访问同一