程序切片是一种重要的、用于分解程序的软件分析理解技术。为丰富程序切片方法,本项目旨在从形式化语义角度研究一种新型的程序切片方法。内容包括(1)模块单子切片理论研究设计一种可统一描述程序切片计算的切片单子转换器,据此研究动态和静态单子切片算法,以及其与传统的基于图可达切片算法间联系;(2)通过这种新型的形式化切片方法研究过程间程序切片,并考虑相应的上下文调用问题;(3)通过将指向分析融入到相应的模块单子切片,研究含指针程序的单子切片;(4)实现模块单子切片算法,开发相应的模块单子切片器原型工具,通过实验数据分析验证单子切片方法的实用性。通过本项目的研究,程序切片这一类计算被抽象成独立于具体语言的切片单子转换器, 它可模块化地加载到实际程序语义描述中, 从而得到相应的模块化和可组合的切片算法。此外,把单子的高抽象、易扩展和修改、重用性等特性"移植"到软件设计与分析中,可为之带来新的思想和观念。例如,我们给出了基于单子技术和切片技术的Web服务形式化模型。这无疑具有重要的科学意义和实际意义。
英文主题词program slicing; formal methods; modular monadic semantics; monads