程序切片是一种重要的程序分析技术,它通过提取程序中直接或间接影响某个特定程序点变量值的语句达到分解程序的目的。随着对程序切片技术研究的深入,其应用领域由软件调试、测试、软件维护扩展到逆向工程、再工程和程序验证等。面向对象技术仍是目前软件开发方法的主流,其中封装、继承、多态、并发等特征都为程序的理解与分析提出了新的问题。本文针对面向对象程序的并发机制,介绍了程序的图形化表示方法——面向对象并发系统依赖图,提出利用变量缓存表分析程序语句间依赖关系的方法,根据分析结果构造面向对象并发系统依赖图,并在此基础上采用改进的两步遍历图可达性算法计算动态切片。程序验证面临的主要问题是由于程序规模的增大,尤其是并发分量的增加,所带来的状态空间爆炸问题。程序切片可以将程序中不影响待验证性质的语句删除以减小针对该程序抽象出的模型的复杂性,从而缩减其对应的状态空间,在一定程度上缓解状态空间爆炸问题。本文提出一种从待验证的线性时序逻辑(LTL)性质中提取出切片准则对程序进行切片的方法,切片后的程序与原程序关于待验证的LTL性质具有相同的可满足性,而其对应的状态转换图中的状态个数明显减少。随着Internet技术和WWW技术的发展,Web应用涉及的范围越来越广,程序规模在不断扩大,其复杂性也越来越高。针对Java Web开发中关键技术的实现机制,把程序切片技术引入到Web应用程序的分析中,定义了Web应用程序中存在的依赖关系,提出了一种构造Web程序系统依赖图并计算程序切片的方法。在以上工作的基础上,本文以Java语言实现的典型并发程序为例对以上提出的方法在实际开发中的应用进行了说明、分析。