基于模块单子语义的程序切片及其关键技术研究

本课题主要从形式化语义角度研究一种新型的程序切片技术。内容包括：(1)将程序切片这类计算抽象成独立于具体语言的切片单子转换器，据此提出一种新型的形式化程序切片方法――模块单子切片（包括动态和静态切片）：可直接在抽象语法结构上计算程序切片、无需在切片器中显示地构造诸如依赖图的中间结构，这种模块化抽象机制使得单子切片算法具有很强的可重用性和组合性；(2)研究模块单子切片的相关理论，包括单子转换器的若干性质、单子切片算法正确性和终止性的证明、单子切片算法与图可达性算法间的联系等；(3)通过这种新型的形式化切片方法研究按值、结果、值－结果调用的过程间程序切片，并考虑相应的上下文调用问题；(4)通过将指向分析融入到相应的模块单子切片，研究含指针程序的单子切片；(5)实现模块单子切片算法，开发相应的模块单子切片器原型工具，通过实验数据分析来验证单子切片方法的实用性。