程序切片是一种程序分析和程序理解技术,它通过寻找程序内部的相关性来分解程序,再通过对分解所得程序切片的分析达到对整个程序的理解.程序切片为开发人员进行软件理解、逆向工程、测试、调试、软件维护、软件度量等提供有效的支持.将程序切片与形式方法结合可以便开发人员更容易理解、分析形式规约和程序代码,从而改进了软件的易维护性和可靠性,也提高了软件的开发效率.该文主要研究程序切片在形式工程方法SOFL中的应用,包括切片技术结合到SOFL方法中的可行性及具体途径.对此,该文做了以下一些工作.首先,该文介绍了程序切片的概念、由来及意义等.由于形式工程方法SOFL是该文的研究基础,也是切片技术被综合应用的框架,该文对SOFL也进行了介绍.●在对SOFL实现的程序进行切片研究时,该文以类Java语言作为基础,研究了在Java语言中实现程序切片的思想,并给出了基于系统依赖图对Java程序进行分层切片的具体算法.●在对SOFL进行规约切片的研究时,该文根据SOFL规约结构,提出三种适应于不同要求的对规约进行切片的方案:整体切片法、分层切片法、综合切片法.