（计算机软件与理论专业论文）模块单子切片性质研究及扩展.pdf

摘要 摘要 程序切片是一种程序分解技术。因目前切片方法缺乏模块性和灵活性，我们实验室 曾提出一种新的形式化切片方法一模块单子切片。目前，模块单子切片的基本理论己 初见规模，但是模块单子切片的一些性质尚未有深入探讨，所处理的语言机制还有待完 善扩充。本文在已有工作的基础上，部分完善了模块单子切片的基本理论，并将之扩展 以处理含指针的程序。 主要工作包括：( 1 ) 模块单子切片算法终止性的精确证明。在现有理论的基础上， 利用指称技术及不动点理论给出终止性证明。( 2 ) 定义模块单子切片与基于依赖图的切 片方法的一致性。( 3 ) 含指针程序的模块单子切片。主要研究内容是切片算法的扩展。 通过将指向分析融入已有的模块单子切片，改进的模块单子切片可以处理含指针的程 序。不同于将指向分析与切片计算分开的传统切片算法，改进的模块单子切片将正向程 序切片思想与数据流迭代分析相结合后，可同时进行切片计算和指向分析，从而保证了 较高的精度，而且比一般的数据流迭代方法节省空间。 关键词：程序切片；模块单子切片；终止性；一致性；指向分析 东南大学硕士学位论文 a b s t r a c t p r o g r a ms l i c i n gi saf a m i l yo fp r o g r a md e c o m p o s i t i o nt e c h n i q u e s b e c a u s et r a d i t i o n a l p r o g r a ms l i c i n gm e t h o d sl a c km e d u l a r i t ya n df l e x i b i l i t y , w eh a dp r o p o s e da n e wf o r m a l m e t h o df o rp r o g r a ms l i c i n g 一m o d u l a rm o n a d i cs l i c i n g a tp r e s e n t ，t h e r eh a sb e e ns o m e r e s e a r c ho nt h eb a s i ct h e o r yo f m o d u l a rm o n a d i cs l i c i n g h o w e v e r , s o m ei m p o r t a n ta s p e c t so f m o d u l a rm o n a d i cs l i c i n gt h e o r yh a v e n tb e e ns t u d y , a n dt h el a n g u a g em e c h a n i s mt h a tc a nb e a d d r e s s e db ym o d u l a rm o n a d i cs l i c i n gi ss t i l ll i m i t e d o nt h i sb a c k g r o u n d ，t h i sp a p e rs t u d i e s t w oa s p e c t so f t h eb a s i ct h e o r yo f m o d u l a rm o n a d i cs l i c i n ga n de x t e n d si tt oh a n d l ep o i n t e r s t b em a i nw o r ki n c l u d e s ：( 1 ) t h ep r o o fo ft h et e r m i n a t i o no fm o d u l a rm o n a d i cs l i c i n g a l g o r i t h m w eo b t a i nt h er e s u l tw i t ht h eu s eo f d e n o t a t i o n a lt e c h n i q u ea n df i x e d - p o i n tt h e o r y ( 2 ) d e f i n i n gt h ec o i n c i d e n c eb e t w e e n t h em o d u l a rm o n a d i cm e t h o da n dt h ed e p e n d e n c eg r a p h m e t h o d ( 3 ) m o d u l a rm o n a d i cs l i c i n gf o rp r o g r a m sw i t hp o i n t e r s n i sp a p e rp r e s e n t sa n a p p r o a c ht oe x t e n dt h em o d u l a r m o n a d i cs l i c i n gf o rh a n d l i n gp o i n t e r s w i t ht h ei l l u m i n a t i o n o ff o r w a r dp r o g r a ms l i c i n g ，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 r m a t i o nb yt h ed a t a - f l o w i t e r a t i o n b e i n gd i f f e r e n tf r o mt h et r a d i t i o n a lm e t h o d sw h e r et h ep o i n t - t oi n f o r m a t i o na n d s l i c i n ga r ea n a l y z e di nt w od i f f e r e n tp h a s e s ，t h e ya r ec o m p u t e di nt h es 姗ep h a s ei no u r m e t h o d , t l 旺o u g hc o m b i n i n gt h ef o r w a r dm o n a ds l i c i n gw i t hd a t a - f l o wi t e r a t i o n 。ns h o w s t h a t 0 1 1 1 a p p r o a c hh a sh i g hp r e c i s i o n ，a n dn e e d sl e s ss p a c ec o m p a r e dw i t ht r a d i t i o n a ld a t a f l o w i t e r a t i o nm e t h o d s k e y w o r d s ：p r o g r a ms l i c i n g ；m o d u l a rm o n a d i cs l i c i n g ；t e r m i n a t i o n ；c o i n c i d e n c e ；p o i n t - t o a n a l y s i s 东南大学学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我 所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成 果，也不包含为获得东南大学或其它教育机构的学位或证书而使用过的材料。与我同工作的同 志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。 研究生签名： 东南大学学位论文使用授权声明 东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复印件和 电子文档，可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内容和纸质论文的内 容相一致。除在保密期内的保密论文外，允许论文被查阅和借阅，可以公布( 包括刊登) 论文的 全部或部分内容。论文的公布( 包括刊登) 授权东南大学研究生院办理。 研究生签名： 第一章引言 第一章引言 1 1 选题依据 随着计算机技术的飞速发展，软件系统的数量越来越多规模越来越大，复杂程度越来越高。 在一些大型、长生命周期的软件测试和维护过程中，手工分析己变得越来越不可行，越来越多的工 作需要理论、技术与工具的支持。程序分析技术已成为软件领域的一个十分重要的研究领域。 程序切片是由m w e i s e r 提出的一种重要的程序分析理解方法【i 一。给定稃序p 、程序点p 和变量 集v ，其切片包含当程序执行到p 时，p 中所有直接或间接对v 中变龟有影响的稃序片断。其中 称作切片标准。移序切片技术已在实际中得到广泛应用，所涉及的领域包括：程序分析、理 解、调试、测试、软件维护、度量、逆向工程、再工程等9 ”。 目前程序切片的算法主要采用基于依赖图的图可达性算法l 6 l 。该方法是顺序增量式的。模块性 较差。针对这一缺点，我们实验室的张迎阁博士从形式化语义的角度考虑了一种新的切片方法 模块单子切片( 下称“单子切片”或“单子切片方法”) 口“。它基于程序的模块单子语义”“通过 将程序切片这类计算抽象成独立于具体语言的切片单子转换器并将之模块化地加载到实际程序语 义描述中，我们可直接在抽象语法项上计算切片，无需在切片器中构造诸如控制流图或依赖图的中 问结构。这种模块化抽象机制使得我们的单子切片具有较强的重用性和程序语言适应性。 目前，模块单子切片的基本理论已初见规模。但是模块单子切片的一些性质尚未有深入探讨， 例如切片算法的终止性问题尚未有证明；而且所处理的语言机制还有待扩充。本文拟在现有单子切 片理论基础上，给出单子切片算法终止性的证明、定义单子切片方法与基于依赖图的切片方法的一 致性、扩展单子切片方法到含指针的程序中，以此完善单子切片方法并推动它的实用化。 1 2 国内外研究现状 1 2 1 模块单子切片 基于程序语义的切片方法源于1 9 8 9 年p a h a u s e r 发表的论文“d e n o t a n o n a l p r o g r a ms l i c i n g ”m 】。 此论文中，他利用指称语义的思想给出了一简单语言的指称切片器。g a v e l l k a t e s h 也注意到了指称 语义在程序切片中的应用，在其1 9 9 1 年a c m 会议论文“t h es e m a n t i ca p p r o a c h t o p r o g r a ms l i c i n g ” ”中给出了程序切片的形式化定义及其算法的指称描述。 传统指称语义缺乏模块性和重用性已为人们所熟知，参见文献 2 0 1 。m o g g i 通过使用单子来加强 语义描述的模块性，单子将诸如状态、环境、异常和不确定性的程序“混杂”特性封装起来，仪允 许由单子所提供的一些操作来访问它们口”。但是，在单子语义中无法将两个单子结合成一个新单子， 为此，e s p i n o s a 重新提出了m o g g i 早期报告中的单子构造器概念，并重命名为单子转换器，它将给定 单子转换成新单子，并增加新操作运算”。此基础上，s l i a n g 等人提出了模块单子语义，使用单子和 单子转换器描述程序语义，将秆序基本概念( 如存储、环境和通信等) 独立地封装在单子转换器里【l ”。 本实验室的张迎周博士利用模块单子语义，研究模块单子切片技术。目前，单子切片方法已能 计算结构化的小型命令式语言的动静态切片，对于“传值”的过程间调用也能进行处理口q 。 1 2 2 含指针程序分析技术 指针的出现可导致别名问题p z 捌( 即多个变量访问同一内存位置) ，故需要进行指针分析以获得 相应的数据依赖信息。指针切片技术的研究主要包括：如何表示像链表这样的递归数据结构? 如何 更新数据依赖的定义以考虑别名情况? 如何进行指向分析来确定变量的指向集? 对于表示递归数据结构的问题，许多学者己提出了解决方法【“，3 5 蚓。这些方法基本上都足利用 某种近似将无限的结构有限化。较粗糙的方法是将堆空间看作一个整体来处理。更精确的做法需采 用形分析( s h a p ea n a l y s t s ) 1 1 5 。 更新数据依赖定义的问题与第一个问题联系较大。由于第一个问题的解决已经保证了对程序中 变量的有限表示，因此可以依据潜在的对抽象内存位置的定义和引用，来定义数据依赖【3 ”。 根据分析时是否采用控制流信息，指向分析可分为流敏感和流不敏感两种。流敏感的分析p r l ， 考虑控制流，需要迭代，故效率相对较低，但精确度较高，可以得到每一程序点的指向信息。而流 不敏感的分析，不考虑控制流，认为程序中的语句可以按任意次序执行，因此它只能为每个变量全 局地( 或在一定范围内) 确定一个指向集，而不能精确到程序点。如文献 3 8 】就是为每个变帚全局地 确定个指向集，文献【3 9 】则为每个变量针对每个过程确定了一个指向集。所以说流小敏感的分析不 东南大学硕士学位论文 够精确，但是它的效率较高，尤其是采用了u n i o n - f r e d 算法后。其效率可以接近线性p ”。 1 3 主要研究内容 本文在现有单子切片理论基础上，进一步完善单子切片的基本理论，并将之扩展到含指针的单 子切片中。主要工作包括； ( 1 ) 单子切片算法终止性的精确证明。 本文拟基于指称语义与不动点理论来严格证明单子切片算法的终止性。主要想法是将切片计算 指称为完全偏序集上的函数，然后再证明切片计算是连续且递增的函数。这样就可以说明该函数存 在最小不动点。接下来考虑集合的有限性就可以证明_ i 幺最小不动点是有限步可求得的即算法终止。 ( 2 ) 定义单子切片方法与基于依赖图的切片方法的一致性 基于依赖图的切片方法应用广泛，因此说明两种切片方法所得切片结果一致对于讨论单子切片 方法的正确性是很有帮助的。本文把两种切片方法的核心计算过程看作一个状态转换过程，并说明 在状态集之间可以建立同态。由此给出两者一致性的定义，为进一步的一致性证明做准备。 ( 3 ) 含指针程序的单子切片方法 上文提到指针的引入给程序分析带来了三个主要问题。本文拟在综合考虑单子切片以及指针分 析的基础上，给出对这三个问题的解决方案，其中着重论述指向分析。通过指向分析、扩展赋值语 句的语法及重新定义引用集来泛化数据依赖，并考虑赋值语句中左值表达式对变量的可能引用情况。 1 4 论文主要成果 论文的主要研究成果表现在以下几个方面： 给出单子切片算法终止性的证明，以完善单子切片理论； 定义单子切片方法与基于依赖图的切片方法的一致性，为研究单子切片方法与基于依赖图的 切片方法问的联系提供了新的思路，也为一致性的证明工作做好了准备； 通过将指向分析融入已有的单子切片，扩展的单子切片方法可处理含指针的程序；主要研究 内容是切片算法的扩展；不同于将指向分析与切片计算分开的传统切片算法，扩展的单子切 片算法将正向柙序切片思想p 1 与数据流迭代分析相结合后，可同时进行切片计算和指向分析 从而保证了较高的精度。而且比一般的数据流迭代方法节省空间。 1 5 论文结构 论文主要由三部分组成：第一部分包括第一章、第二章和第三章，综述全文，介绍模块单子语 义以及程序切片的基本概念，并简要介绍已有的模块单子切片算法：第二部分包括第四章，证明单 子切片算法的终止性，定义单子切片与依赖图方法的一致性；第三部分包括第五章，扩展单子切片 方法，以求含指针程序的单子切片。各章节摘要如下： 第一章是全文的绍论，从切片技术的发展等方面入手分析问题来源。介绍单子切片方法的来由 及其尚存的不足；描述论文的研究方案，在给出研究内容和方法后，简要介绍研究成果和论文结构。 第二章介绍一些通用的概念，包括单子和单子转换器等梭块单子语义相关的概念；还包括程序 依赖图、数据依赖、控制依赖、切片分解定理等程序切片相关概念。 第三章简要介绍已有的模块单子切片。首先设计一种切片单子转换器。此基础上，提出切片算 法，给出其详细的步骤，并分析算法复杂度。 第四章证明第三章所介绍算法的终止性，并定义单子切片方法与依赖图方法的一致性。拟基于 指称方法与不动点理论来严格证明算法的终止性。在一致性定义方面，准备说明依赖图作为状态包 含了更多的信息。只能给出依赖图到切片表的同态映射。 第五章研究含指针程序的单子切片技术，通过指向分析、扩展赋值语句的语法及重新定义引用 集来泛化数据依赖，并考虑赋值语句中左值表达式对变量的可能引用情况。采用流敏感的数据流迭 代方法来分析指向，具有了较高的精度，而且不需要像一般的流敏感分析方法那样记录每个程序点 的指向信息，而是随着切片分析同时记录相应指向信息，从而节省了存储空间。 第六章是对全文研究工作的总结，综述本文在模块单子切片研究领域获得的成果，并且指出我 们现有工作的局限性以及有待提高和改进的方面。简要阐述我们正在进行或将要进行的研究工作。 2 第= 章基本概念 第二章基本概念 本章主要讨论与模块单子语义和程序切片相关的一些基本概念。单子和单子转换器是模块单子 语义中最基本的两个概念，单子用来替代 表示法以加强语义描述的模块性，单子转换器可解决多 个单子结合问题。此外，我们还介绍目前在切片系统中应用晟广泛的程序依赖图和切片的有关概念。 2 1 模块单子语义 指称语义是种强大的研究程序设计语言语义形式化的数学方法，它对设计和执行程序以及推理 程序性质等都是非常有用的。在描述指称语义中所使用的形式化表示法是 表示法，指称也是由 表达式给出的高阶函数。 但是，正因无约束地使用 表示法描述语义实体，使得传统指称语义缺乏模块性和扩展性 2 0 1 。 当对所描述语言的结构进行很小扩展时其指称论域需要作相应改变，并且为了适应新的论域，必 须全部重写扩展前的语义描述。为加强语义描述的模块性，避免定义结构语义时对无关语义成分的 引用，必须采用更加规则的表示法来替代 表示法，单子就是其中的一种方法。为了使用单子来描 述程序语义，常使用单子转换器来结合多个单子。这种方法称为模块单子语义( m o d u l a rm o n a c h c s e m a n t i c s ) ，它使用单子和单子转换器描述程序语义，将程序基本概念( 如存储、环境和通信等) 独 立地封装在单子转换器里。， 2 1 - 1 单子 单子( m o n a d ) 1 9 5 0 年代已被作为范畴论里一种函子，但直到1 9 8 9 年才由e m o g g l 将之引入到 语义描述框架中【2 l 】。在m o g g i 的系列报告中，他用单子表示了程序讶算的一些基本概念，如：环境、 状态、输入输出、连续统、不确定性等。随后，e w a d l e r 将m o g g t 的单子方法广泛推广到函数式 程序设计( 尤其是h a s k e l l 语言) 中【捌。采用单子这种更加规则的表示法替代 表示法，可避免定义 语义结构时对无关语义成分的引用，从而加强了语义描述的模块性和扩展性。 单子是种抽象技术，它可隐藏计算时所需的基本信息，并提供一些( 操作) 函数允许外界访问 这些信息。虽然单子的概念来源于范畴理论，但单子可进行如下形式化地定义i z “： 定义2 1 个单子m 是一个三元组沏，r e t u r n m ，b i n d m ) ，包括类型构子m 和两个多态函数： r e t u r n m ：a 埘a b i n d ： m 4 寸0 - 妨r d b 且它们满足如下规律； 左幺元：( r e t u r n md 1 b i n d m k = k a 右幺元： m b i n d r e t u r n m = m 结合律： m b i n d m ( h ( t 口) b i n d m ( x b h 堋= ( 6 z h 厶( h k 口) ) b i n d m ( 柚h 这里的b i n d 是函数b i n d m 的中缀表示，即表达式a b i n d m b 恒等于b i n d mab 。口b i n d ( h 6 ) 的直 接含义为：先计算a ，将其结果传给变量y ，此基础上再计算b 。r e t u r n 。a 表示一种平凡计算：对a 不作任何的计算，仅返回值a 。 直观上。对于类型口，类型ma 则表示所有能得到a 类型结果的计算，这些计算在范畴理论的 同态概念下是一致的。因此，可以说，给定一个单子实际上就相当于给定了能够得到某种类型结果 的计算类型p j 。 现在，单子已是独立的概念，掌握它不再需要范畴论的知识，而且大量的研究和实践已证实单 子系统具有很强的功能，结合单子表示法的简洁性和易读性，因此将为越来越多的人所接受和应用。 将单子概念引入程序设计的重要意义不仅在于它的独特描述方式，而更为重要的是它将成为程序设 计带来新的思想和观念。有人认为单子技术可作为程序设计的通用技术来使用。 为了更方便地使用单子，本文余下部分将采用如下的简写形式，它类似于函数式语言h a s k e l l 2 5 1 的d 0 表示法 忙 删；p 仁- 成；p l e t e x p ；p e m b i n d x 。 e l r l l b t n d z e i l e t e x p i n p 3 东南大学硕士学位论文 2 1 2 单子转换器 在使用单子描述程序语义时无法将两个单子结合成一个新单子，从而限制了单子语义的进一 步扩展，一个可行的解决方法是使用单子转换器，它将给定单子转换成新单子，并增加新操作运算。 在m o g g i 的早期系列报告中，他意识到，实际的语义特性应该能进行组合，为此他提出了可给一个 单子增加新的计算信息的单子构造器( m o n a d c o n s t r u c t o r ) 概念。后来，d e s p i n o s a 【i8 】在其博士论文 中将之重新命名为单子转换器( m o n a d t r a n s f o r m e r ) ，并一直沿用至今下询是单子转换器的一种形 式化定义： 定义2 2 单子转换器由类型构造器t 及其提升函数确构成。其中t 将给定的单子伽，r e t u r n 。， b i n d s ) 映射到新单子( t m ，r e t u r n ，卅，b i n d t 。) ，提升函数t o , ： 确：m a - t m a 还要满足： u f t , 摧唧删= r e h l r ? l r m 啪( b m d 。m 妨= b i n d t 。( 坼m ) ( 坼助 单子转换器不仅提供了一种抽象化表示程序特性的能力，而且还允许人们访问低层语义的细节 部分。概念“提升”使得我们能考虑不同程序特性问的交互。单子转换器的两个规律保证了提升的 基本性质：对任何一个程序，如果不使用由单子转换器所引入的新特性，则在单子转换器作用前后， 该程序的表现行为应该一致。 因单子转换器完全独立予具体语言，仅表示某类计算，故单子转换器的设计复用性很强田】。目 前人们已设计了不少单子转换器【1 9 , 2 1 ，如图2 1 所示。 环境单子转换器；状态单子转换器：- t y p e e n v t p m d = 户 m at y p e $ 1 a t e t s 辨4 l f + m o ，4 ) r e l u r n 鲥r 口_ z 。九肛r e t u r n m xr e t u r n s t “r j _ z= h r e l u r n _ o ，曲 j b m d 酣r 口- fz 口扣- j p ；f a 西_x b j 耐鼬盯，_ f = h o ，a ) - j 5 ；f a ， _ 妒嘶t ，j= 扣j b m d _ r e t u r n mt j j = h 扣卜j ；r e t u r n _ o ，口) ) _ r d e n v = z p r c l u r n a pu p d o z ef= h ，r e t u r n m o s ，曲 i n e n v p x= l j p 错误获取单子转换器： i o 单子转换器； t y p e e r r a = o ka i e r r s t l a n g t y p e i o t md ；s t n n g - j ，l d ，s t 6 n g ) t y p e e r r t i n d 。m ( e r r 4 ) r e t u r n l 竹_ 4。h r e l u r n 0 ，曲 r e t u r n f * t m x 2r e t u r n _ ( o k x ) x b i n d e r ，= k s ( d ，5 ) 4 - x $ ；，口j ) _ j 6 l 珊k _ l t _ f4 4 。；! 。辣4 0 f 够l o t ，j= h 口卜墨r e l u r w _ 0 ，印 _ u k y ：，y 一 、g e t v a l u e= b 撑鲫w o ，订 ，e r r sr e t u r n m 衄s ) - p u t v a l u ej ；l m 赢i o ) 题厅h 亓j= 忙4 - x ；r e l u r n _ ( o k d ) ) _ 一 e r rs r e l u r n _ ( e i rs ) 图2 1 一些常见的单子转换器 2 1 3 模块单子语义 模块单子语义通过将语法项映射到计算( 单子) 来形式化描述程序语义，通常包括两个部分： 语义构造块和单子转换器。语义构造块独立且模块化地定义程序的每个结构，而单子转换器则模块 化地定义相应的核心性质。代表不同计算特性的多个单子转换器可被一起组合到语义构造块的基本 单子中，使得该基本单子包含所有的程序特性，于是可用之描述高级语言的语义。 单子转换器由通常的指称语义描述。多个单子转换器可结合到一个基本单子中，从而使得最终 单子包含了所有要描述的程序概念。模块单子语义与传统指称语义的区别在于：模块单子语义中的 单子都是独立实体，其模块可进行独立验证。并且某个模块相关命题的证明，在其它模块被改变、 增加和删除情况下也无需重新进行。可见，模块单子语义具有了真正意义上的模块性，这将有利 于对语义描述的重用和增量式修改。 为了讨论单子切片，现引入一个实例语言w ，它类似于文献 2 6 】中的语言，包括赋值、分支选 择、循环、结构块、输入输出和声明等语句，其抽象语法见图2 2 。为不失一般性，图2 2 中没有给 出具体的表达式b n f 范式，并假设表达式没有诸如赋值等的副作用。为方便后面讨论，赋予每个表 4 第二章基本概念 图2 2 实例语言w 的抽象语法 v ：v a l u e ( 值域) ；o c ：l u e ( 存储) ；j ：s t a t e ( 状态) ； 肛e n v ( 环境) 语义方程： m ：p r g c o n l p t m 0 材p r e g r s m i d e b b = 戚b 矗：b i k _ c o m p t m 0 矗d b 唯hce n d t ，一口d ；i n e n v f f c c d ：d e c _ c o m p t m e n v 五：e x p i c o m p t m v a l u e d c o a s t i d e = 1 c t v 矾1 e ；p - r d e n v ；r e l u r n , 4 v i d e d - 扣- 层l ，c ；z i d e n v o d e ，r e t u r n h r d e n v ) d v - r i d e ：t 。 f o c a l l o c ；x m e n v ( u i e ，r e t u r n l o c r d e n v ) d d l ；屯- 户十柑砌巧f f + - i n e n v p d d 1 i ；r e t u r n ( i n e n v f f d ed 2 1 ) c ：c m d c k m l p d v l 0 d i d c ：= 1 ，c = 扣+ - 层1 o ；胁r - l k p e n v ( i d e ，n t e n v ) ；u p d s t o ( 1 0 c , r e l u r n 啪 c e l ；c 2 = f c c - ；c c 幽口= r e t l r n 0 c 1 1 1 c t h e n c i 出ec 2 e n d i f i 。f y i c ：v = t t _ c c l l ，c c 2 ) c w h i l e l c d o c a d w h l l e = ，k ( v v 卜i c ：v = t t 斗，c c l ，r e t u r n 0 ” c u n m d i i d e m = ，o c r l k p e n i i d e , r d e n v ) ；vj - - g e l v a l u e ，u m s z o ( 1 0 c ，r e t u r n 力 c w r i t e l ，e = v 一量1 e ) ；p u t t ：d u e ( r e t u r n j 图2 3 实例语言w 的语义构造块 达式一个唯一标号，且该标号是针对整个表达式的，其子表达式不再有标号。为后面计算切片方便， 对r e a d 语句中变量也赋予一个标号。以下关于切片的讨论都是基于w 语言展开的。 在模块单子语义描述中，单子是由作用在某基本单子上的单子转换器组合定义的。这个基本单 子通常是预先定义的输入，输出单子i o 或恒等单子i d 。本文采用单子i o ，并考虑程序的环境、状态、 错误获取等计算特性，它们分别由图2 1 中的e n v t , s t a t e t , e r r t 等单子转换器表示，然后一起复合 成了相应语义构造块中的最终单子c o m p t m ： c o m p t m # ( s t a t e t e n v t e r r t ) i o 这样。结合图2 1 中的单子转换器，图2 3 就给出了实例语言w 的模块单子语义。图2 3 中 标识符f x 为不动点算子；i k p e n v 是环境域e a r 中查找操作；u p d s t o 是存储域l o c 的更新操作 2 2 程序切片 m w e i s e t 于1 9 7 9 年在他的博士论文( 。p r o g r a ms l i c i n g ：f o r m a l p s y c h o l o g i c a l ，a n dp r a c t i c a l i n v e s t i g a t i o n s o f a n a u t o m a t i c p r o g r a ma b s t r a c t i o n n t h o d ”) 中首次提出程序切片概念”，并在1 9 8 4 年 s 东南大学硕士学位论文 的i e e e 重要杂志( i e e e t r a n s a c t i o n so ns o f t w a r ee n g i n e e r i n g ) 发表文章迸一步阐述了程序切片的思 想和实现算法【2 】。w e i s e r 等人经研究发现，程序的某一个输出只与源程序中部分语句和谓词有关， 删除其它的语句和谓词并不影响该输出的结果。他们把这种只与某个输出有关的语句和谓词构成的 程序称为源程序的一种静态切片，并提出了基于控制流图( c f g , c o n t r o l f l o w g r a p h ) 的程序切片算 法。k o t t e m t e i n 等人【l ”于1 9 8 4 年引入了基于程序依赖图( p d gp r o g r a md e p e n d e n c eg r a p h ) 的图 形可达性算法，以此来计算过程内后向切片( b a c k w o r d s h c m g ) 。s h o r w i t z 等人”1 ”1 分别于1 9 8 8 年 和1 9 9 0 年提出了前向切片( f o r w o r d s l i c i n g ) 概念及其算法。 定义2 3 对程序p 、程序点s 和变量集v 。其切片是由籽序p 中的部分语句组成，这些语句的 执行可能影响s 处v 中变量的值。其中， 称为一切片标准。 程序切片分为两种：静态切片和动态切片。静态切片考虑程序所有可能的执行情况，与其输入 无关；动态切片只分析对给定输入、程序动态执行时所经过路径上的语句，随输入的不同而会发生 变化。因为单子静态切片的性质与扩展的研究较有代表性，敌本文主要的研究对象是单子静态切片， 如未特别说明，本文提及的单子切片均是指静态切片。 程序切片还可分为后向切片和前向切片。后向切片包含影响变量的所有语句和谓词：前向切片 包含受该变量影响的所有语句和谓词。本文主要讨论后向切片。 由于顺序程序中依赖关系具有传递性，基于p d g 的子程序内切片算法是个图的可达性问题l l ”。 相关定义如下： 定义2 4 程序p 的p d g ，记为g h 是一个有向图( k 日，v 为节点集，p 中每个语句都对应图 中的一个节点：e 为边集，表示节点间的依赖关系。如边a _ b 表示节点a 和b h j 存在依赖关系， 并称o 为该边的源点，b 为目标点。 g ，的节点，记为h g 尸) ，一般为程序中出现的赋值语句和控制谓词。此外，h 鳓还包含一类被 称作入口顶点的节点。g p 的边，记为目g 户) ，包含控制依赖边和数据依赖边。 定义2 5 设v l 与v 2 是程序p 的两个语句，若也的执行与否取决于v l ，则称v 2 控制依赖于v l ， 记为v l bv 2 。 定义2 6 设a 是语句v 中定义的变量，如果a 在v 1 中的变化可能影响到语句屹中变量b 的定 义或引用，则称v 2 中的变量b 数据依赖于中定义的变量a ，记为kv 2 。 定义2 7 一个程序依赖图g 关于节点s 的切片，记为g s ，是包含能通过数据依赖边和控制依 赖边至0 达j 的所有节点的图，其节点集h g s ) = w l w _ 。d j ，w e h g ) 。 图2 4 个简单程序及其p d g 图2 4 是一个简单的p d g 示例。图中e n t r y 是入口顶点，带阴影部分为程序最终处变量x 的切 片。 定理2 1 ( 分解定理) 对程序点的任意集合u 曲，有u ( g s j ) 。g u & 。 6 第三章模块单子切片方法 第三章模块单子切片方法 本实验室的张迎周博士针对目前程序切片方法较单一。且模块性较差的缺点，提出了基于模块 单子语义的切片方法。通过单子转换器，切片这一类计算被抽象成独立于具体语言的切片单子转 换器，它可模块化地加载到实际程序中得到相应的单子切片算法。本章将简要介绍这种新掣的形 式化程序切片方法：准备给出切片单子转换器、模块单子切片算法的详细步骤并分析算法复杂度。 3 1 切片单子转换器 ，文 3 0 给出了一种切片单子转换器，其具体定义见图3 1 所示。图31 中+ 为单元类型u n i t 中唯 一的元素：表示进行当前语句计算所需表达式的标号集合；j 为切片表s h c e s ，其数据结构如下： t y p e v a r = s t n n g t y p e l a b e l s = h t 】 t y p es l i c e s2 【w a r , l a b e l s ) l k p s h ：v a r _ s l i c e s _ c o m p t ml a b e l s u p d s l i ：( v a t , c o m p t ml a b e l s ) _ s l i c e s _ c o m p t m0 m r g s l i ：s h c e s _ s l i c e soc o r n p t ms l i c e s 每个变量所对应的切片是一个标号集合，所有变量及其切片构成了一张表( h a s h 表) ，记为切片类 型s l i c e s 。它包括三个基本的操作函数：t k p s l i 、u p d s l i 和m r g s l i ，分别用来查找s h o e s 中某变量对应 的切片( 标号集合) 、更新s h c e s 中数据和合并两个s h c 2 s 。 切片单子转换器s l i c e rlj 以 标号集合和切片表j 作为参数， 返回的是一类计算，该类计算的结 果由是终计算值和切片表构成。其 中基本操作r e t u r n s l m 返同原来给 定的值，且对切片表不作任何修 改。操作b i n d s l 。d 先接受两个参数： 单子i n 和函数 并将标号集合l 和切片表s 传递给单子m ，产生计 算值a 和中间切片表s ，再将函数 f 作用到值a 上，产生单子f a ，最 后该单子在l 和s 吓计算得到最终 的值和相应的切片表。 r d l a b e l $ i n l a b e l s 和g e t s l i , s e t s l i 分别是s h c 2 t 中参数和j 的馈取和更新操作。 提升函数a s i ，w 说的是，为在单子s h e e t l j m 下计算m ，先保留初始切片表j ，再计算m ，然 后将计算值a 及j 一起作为结果返回。 通过切片单子转换器s h e e t ，其它的单子( 如状态单子s t a t e m o n a d 和环境单子e v n m o n a d ) 可 很容易地被转换成切片单子s l i c e m o n a d ： t y p es h c e m o n a da ；( l a b e l s ，s h c e a ) _ q ，s l i c e s ) ? 2 t u r nj ；m 厶s ) 似曲 m b i n d f = m ，j ) ( d ，j ) + - m 伍，s ) ；f a 以s 7 ) 这可通过提升单子中相应的操作来完成。如s h e e t 对环境单子e n v m o n a d 、状态单子s t a t e m o n a d 、 错误获取单子e r r m o n a d 和输入输出单子i o m o n a d 的提升可分别表示为： i n e n v s b c e t lj mp x = 犯，曲m e n v = p 0 犯，j ) ) ： r d e n v m l c o t l j m = l l j 疗s l l c e t l j r d e n v m u p d a t e s = l w j m；l i f t s j ，“t j u p d a t e m ； g e t v a l u e s h c e t l j _= ，珞i 。日l 。g e t v a l u e m ；p u t v a l u e s l m r j _ = l i f t s l i e e t l j p u t v a l u e m e r r s l i t l ，m。i a s l r l je r r i 同样地，其它单子转换器t 也可将s h c e m o n a d 转换成其它相应的单子。 3 2 单子切片算法 程序中某个变量的静态切片将包括所有可能影响该变量的值计算的语句，它是通过分析程序的 源代码来获取程序的有关信息。本章介绍的单子切片仅考虑程序执行最终点的单变量程序切片，对 应静态切片标准为：印，v ，其中p 为程序最后语句点；v 为程序中某个变量。由切片分解定理2 1 7 东南大学硕士学位论文 知，通过合并相应单个变量的程序切片，可易得到多个变量的程序切片”。 3 2 1s y n o ，工) 的定义 为了讨论切片，图3 2 给出了w 语言的s y n ( s ，l ) 刚9 3 ( 0 0 1 ，其中s 表示被分析的w 源程序：r e # 0 c ) 表示所有出现在表达式1 e 中变量的集合；s 表示空操作。s y n ( s ，) 说明了如何根据切片表中标号集 合，从源程序s 中构建一个符合语法的w 子稃序，即相应的程序切片。置( s ，d 允许我们只需关 注所分析程序中的加标表达式，因为程序切片主体部分依赖于语句中的表达式，其它部分可由s y n ( s ， ) 捕 图3 2 其实只是给出了由l 返回最终切片的一种策略，它还可据不同用户需要作相应修改。如 为了最终切片可执行，可将变量类型声明部分改写成： 血：1 ”：讧血6 ” u m 脚( 1 。) 血。1 出：”。k 5 3 2 2 具体算法步骤 模块单子静态切片算法的基本思想3 0 】是：先将切片单子转换器组合到语义模块描述中，使其包 含程序切片计算然后按此语义描述逐句分析源代码并计算相应的静态切片，最后得到所要求的切 片。算法3 1 描述了计算静态切片 的基本步骤，共分四步。 步雾是求静态切片准备工 作：将标号集合l 及表s l i c e s 中所 有集合初始化为空集。 勇 箨2 目的是将切片计算模 块化地加到程序分析中，这里是通 过我们所定义的切片转换器 s l i c e t 实现的。就本文前一章( 第 2 1 3 节) 所提及的w 语言而言， 就是要将s l i c e t 组合到晟终单子 输入：静态切片标准( p ，v 输出：静态切片 1 初始化标号集合工和s l i c e s 中