程序切片是一种程序分解技术。因目前切片方法缺乏模块性和灵活性,我们实验室曾提出一种新的形式化切片方法——模块单子切片。目前,模块单子切片的基本理论已初见规模,但是模块单子切片的一些性质尚未有深入探讨,所处理的语言机制还有待完善扩充。本文在已有工作的基础上,部分完善了模块单子切片的基本理论,并将之扩展以处理含指针的程序。主要工作包括:(1)模块单子切片算法终止性的精确证明。在现有理论的基础上,利用指称技术及不动点理论给出终止性证明。(2)定义模块单子切片与基于依赖图的切片方法的一致性。(3)含指针程序的模块单子切片。主要研究内容是切片算法的扩展。通过将指向分析融入已有的模块单子切片,改进的模块单子切片可以处理含指针的程序。不同于将指向分析与切片计算分开的传统切片算法,改进的模块单子切片将正向程序切片思想与数据流迭代分析相结合后,可同时进行切片计算和指向分析,从而保证了较高的精度,而且比一般的数据流迭代方法节省空间。