模块单子切片性质的研究及其扩展.pdf

曾提出一种新的形式化切片方法一模块单子切片。目前,模块单子切片的基本理论己要摘程序切片是一种程序分解技术。因目前切片方法缺乏模块性和灵活性,我们实验室初见规模,但是模块单子切片的一些性质尚未有深入探讨,所处理的语言机制还有待完善扩充。本文在已有工作的基础上,部分完善了模块单子切片的基本理论,并将之扩展以处理含指针的程序。主要工作包括:?榈プ忧衅惴ㄖ罩剐缘木分っ鳌T谙钟欣砺鄣幕∩希利用指称技术及不动点理论给出终止性证明。ㄒ迥?榈プ忧衅牖谝览低嫉那片方法的一致性。刚氤绦虻哪?榈プ忧衅V饕Q芯磕谌菔乔衅惴ǖ睦┱埂通过将指向分析融入已有的模块单子切片,改进的模块单子切片可以处理含指针的程序。不同于将指向分析与切片计算分开的传统切片算法,改进的模块单子切片将正向程序切片思想与数据流迭代分析相结合后,可同时进行切片计算和指向分析,从而保证了较高的精度,而且比一般的数据流迭代方法节省空间。关键词:程序切片;模块单子切片;终止性;一致性;指向分析摘要
〆..鷒—甇,:甒.,:籺;Ⅱ
东南大学学位论文使用授权声明东南大学学位论文独创性声明研究生签名:本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知,除了文中特别加以标注和致谢的地方外,论文中不包含其他人已经发表或撰写过的研究成果,也不包含为获得东南大学或其它教育机构的学位或证书而使用过的材料。与我~同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学位论文的复印件和电子文档,可以采用影印、缩印或其他复制手段保存论文。本人电子文档的内容和纸质论文的内容相一致。除在保密期内的保密论文外,允许论文被查阅和借阅,可以公布ǹ论文的全部或部分内容。论文的公布ǹ授权东南大学研究生院办理。
第一章引言国内外研究现状选题依据较差。针对这一缺点,我们实验室的张迎阁博士从形式化语义的角度考虑了一种新的切片方法——.?,,复杂程度越来越高。在一些大型、长生命周期的软件测试和维护过程中,手工分析己变得越来越不可行,越来越多的工作需要理论、技术与工具的支持。程序分析技术已成为软件领域的一个十分重要的研究领域。程序切片是由甒岢龅囊恢种匾5某绦蚍治隼斫夥椒ā綢一。给定稃序⒊绦虻鉖和变量集淝衅背绦蛑葱械絇时,兴兄苯踊蚣浣佣詖中变龟有影响的稃序片断。其中.,称作切片标准。移序切片技术已在实际中得到广泛应用,所涉及的领域包括:程序分析、理解、调试、测试、软件维护、度量、逆向工程、再工程等薄目前程序切片的算法主要采用基于依赖图的图可达性算法8梅椒ㄊ撬承蛟隽渴降摹D?樾模块单子切片鲁啤暗プ忧衅被颉暗プ忧衅椒ā口“。它基于程序的模块单子语义”“.,我们可直接在抽象语法项上计算切片,无需在切片器中构造诸如控制流图或依赖图的中问结构。这种模块化抽象机制使得我们的单子切片具有较强的重用性和程序语言适应性。目前,模块单子切片的基本理论已初见规模。但是模块单子切片的一些性质尚未有深入探讨,例如切片算法的终止性问题尚未有证明;而且所处理的语言机制还有待扩充。本文拟在现有单子切片理论基础上,给出单子切片算法终止性的证明、定义单子切片方法与基于依赖图的切片方法的一致性、扩展单子切片方法到含指针的程序中,以此完善单子切片方法并推动它的实用化。“此论文中,他利用指称语义的思想给出了一简单语言的指称切片器。,在其年嵋槁畚摹癟‘”中给出了程序切片的形式化定义及其算法的指称描述。传统指称语义缺乏模块性和重用性已为人们所熟知,参见文献。ü褂玫プ永醇忧语义描述的模块性,单子将诸如状态、环境、异常和不确定性的程序“混杂”特性封装起来,仪允许由单子所提供的一些操作来访问它们口”。但是,在单子语义中无法将两个单子结合成一个新单子,为此,重新提出了缙诒ǜ嬷械牡プ庸乖炱鞲拍睿⒅孛5プ幼;黄鳎ǜ单子转换成新单子,并增加新操作运算¨”。此基础上,甃等人提出了模块单子语义,使用单子和单子转换器描述程序语义,将秆序基本概念绱娲ⅰ⒒肪澈屯ㄐ诺独立地封装在单子转换器里【薄本实验室的张迎周博士利用模块单子语义,研究模块单子切片技术。目前,单子切片方法已能计算结构化的小型命令式语言的动/静态切片,对于“传值”,故需要进行指针分析以获得相应的数据依赖信息。指针切片技术的研究主要包括:如何