程序切片是由WeiserM.提出的一种重要的程序分析和理解的方法，用于从源程序P中抽取对程序中特定点p上的特定变量V有影响的语句和控制条件，组成新的程序(称作切片)，然后通过分析切片来分析源程序的行为，其中〈p，V〉称作切片标准。程序切片技术的研究、发展和应用已经经历了二十多年，众多学者对切片技术作过专门的研究和应用开发，并且取得了一些具有理论和应用价值的成果，使得它在程序分析、理解、优化、调试、测试、度量、复用、程序变换、模型检查、软件安全、软件维护、软件逆向工程、软件再工程中得到了广泛应用。 随着人们对切片技术的进一步研究，切片的概念不断延伸，切片应用范围也在不断扩大。现在切片技术已经不仅仅是对程序源代码的分析，而是已经应用到形式规约、UML和软件体系结构等方面。OdaT.和ArakiK.最早于1993年把程序切片的思想引入到Z形式规约中去；随后ChangJ.和RichardsonD.J.于1994年在此基础上把形式规约切片划分为静态形式规约切片和动态形式规约切片；紧接着LeminenJ.研究了数据切片，并在此基础上把OttL.的基于程序切片的模块内聚性度量方法应用到形式规约的内聚性度量中。 论文研究详细讨论了已有的程序切片和依赖性分析技术，结合国内外在形式规约切片及其应用方面的研究现状，对形式规约切片及其应用的若干关键技术进行了深入研究，提出基于依赖性分析的Z形式规约切片和基于关系演算的Z形式规约切片，并在此基础上把Z形式规约切片应用到提升、定理证明和度量上，在一定程度上帮助人们对形式规约的分析与理解。论文主要工作有： 1.基于依赖性分析的Z形式规约切片 提出了一种基于依赖性分析的Z形式规约切片方法；该方法分析了传统的数据依赖和控制依赖。数据依赖是变量的定义和使用的属性；如果数据通过一系列的状态变化可从谓词p1传播到谓词p2，则称谓词p2数据依赖于谓词p1。数据依赖可以发生在相同的谓词之间，也可以发生在不同谓词之间；如果数据依赖发生在相同的谓词之间，则谓词肯定在同一模式中出现；如果数据依赖发生在不同的谓词之间，则谓词既可以出现在同一模式中，又可以出现在不同模式中。控制依赖是形式规约的控制结构的属性；如果谓词p1潜在地决定了谓词p2适用与否，则称谓词p2控制依赖于谓词p1。因为if-then-else是Z语言中的主要控制结构，所以控制依赖可以发生在if-then-else中。为了更好地描述Z形式规约和强调操作模式发生时应满足的条件，除了分析传统的数据依赖和控制依赖外，我们引入一种新的依赖关系——逻辑依赖，是由操作模式的前置条件引起的，是控制依赖的一种特殊形式。直接逻辑依赖可以发生在模式内，不能发生在模式间；间接逻辑依赖发生在模式演算中。 虽然对Z形式规约的各种依赖情形进行了分析，但只有这些信息还不足以对Z形式规约进行切片分析，而且这些信息也是杂乱的，因此论文对于模式和形式规约分别引入模式依赖图和形式规约依赖图的概念把这些信息图形化地表示出来以帮助理解。一个模式表示成一个模式依赖图，含有一个入口节点表示模式的入口，节点表示谓词，边表示谓词的各种依赖关系。为了表示千差万别的模式的使用方式，论文借鉴类的使用方式，使用一个框架来模拟所有可能的模式的使用情况。框架首先调用初始状态模式，然后进入一个循环，在该循环中对各种模式进行调用，在通过循环的每个重复中，控制能够传递到任何地方的模式中。初始状态模式、框架循环都控制依赖于框架入口节点，框架循环也控制依赖于自身，这样就形成了形式规约依赖图。在模式依赖图和形式规约依赖图的基础上分别利用图形可达性算法和两阶段图形可达性算法就可以求解Z形式规约切片，切片结果具有较高的精确度，没有丢失必要的信息。 2.基于依赖性分析的Z形式规约切片的形式化描述 为了解决程序切片可能存在的语义不一致性和模糊性，帮助人们正确地理解程序切片的含义，从比较严格的意义上明确程序切片的应用领域，对基于依赖性分析的程序切片进行了形式化描述。首先对程序中的语句和变量进行形式化描述；其次对于目前流行的两种程序切片的定义，即WeiserM程序切片和OttensteinKJ程序切片定义进行形式化描述；之后对程序依赖图和系统依赖图的两个重要组成部分，节点和边按照不同类型和不同形状进行形式化描述；最后对于基于程序依赖图的图形可达性算法和基于系统依赖图的两阶段图形可达性算法进行形式化描述。 依据SloaneAM提出的广义程序切片的概念可知形式规约切片是程序切片的一种特殊形式，所以对于程序切片的形式化描述同样也可以应用于形式规约切片，这样就可以借助一些Z的辅助工具帮助解决切片问题。 3.基于关系演算的Z形式规约切片 提出了一种基于关系演算的Z形式规约切片方法。对于Z形式规约中每个模式s引入三个关系，二元关系MOD(s)、三元关系USE(s)和二元关系CONTROL(s)来辅助切片的求解过程，主要利用关系代数的选择、投影和连接等运算和Z语言自带的关系运算，如，定义域限定、值域限定、求关系的定义域和值域等运算来计算模式前向切片和模式后向切片，把计算切片的过程演变成关系演算的过程。该切片方法避免了构造依赖图的费时费力，降低了出错的机率。 4.变量定义和使用情况的探讨 变量定义和使用情况的分析是论文第二章计算数据依赖与控制依赖和第四章计算数据依赖的基础。鉴于Z语言基本的赋值运算符有：集合定义符“==”、关系定义符“==”、函数定义符“==”、枚举型定义符“∷=”和标准定义符“=”等，而且Z语言使用一阶谓词逻辑、集合、关系、映射、序列和包等表示法来描述系统，所以我们首先借助已有的数学公式、定律和定理对表达式进行化简，然后分别讨论这些数学抽象对变量的定义和使用情况。变量定义分析的任务是找出每个谓词中形式上的赋值变量，使用变量分析就是要找出一个表达式到底依赖了哪些变量。论文采用一个递归分析的方法，逐层找出加在基对象上的操作类型，最后这些操作综合起来就可以找出定义变量和使用变量的情况。 5.Z形式规约切片在提升和定理证明中的应用 把Z形式规约切片应用到提升中去，给出了一种求解提升模式Promote的公式，实现了形式规约的结构化，这样就可以用局部操作模式和提升模式来描述全局操作模式，而不必把每一个全局操作模式都罗列出来。 把Z形式规约切片应用到定理证明中去，把定理证明的过程转化为以结论为切片标准的后向Z形式规约切片的过程。 6.基于依赖性分析的Z形式规约度量 在模式依赖性分析的基础上提出一组针对Z形式规约的耦合性度量准则。该组度量准则考虑了模式修饰、模式包含、模式演算和模式作为类型等多个方面。为了验证度量准则与人们经验的一致性，论文用交通车辆管理系统作为案例来讨论。为了更好地说明提出的Z模式耦合性度量与其它度量的联系同时考察了著名的CK度量，并比较这两种度量在评估系统时的优劣。试验结果表明该度量准则与人们广泛接受的CK度量显著相关，与人们的经验具有高度的相关性；根据这些度量准则可以发现一些问题，并把问题杜绝在软件开发的早期阶段，减少由于错误或不合理分析导致的浪费，并可对系统进行有效的评估。 论文主要的创新点有以下三个方面： 1.提出一种基于依赖性分析的Z形式规约切片方法。在该方法中，除了分析传统的数据依赖和控制依赖外，为了强调操作模式的前置条件，论文引入了一种新的依赖关系——逻辑依赖。之后，鉴于Z形式规约没有类似程序代码的“主程序”的原因，采用面向对象系统依赖图的形式对其进行图形化表示；对于模式和形式规约分别引入模式依赖图和形式规约依赖图的概念。在此基础上给出了一种有效的基于依赖图可达性分析的Z形式规约切片方法，该方法具有较高的精确度，没有丢失必要的信息。 2.提出了一种基于关系演算的Z形式规约切片方法。该方法主要利用关系代数的选择、投影和连接等运算和Z语言自带的关系运算，如，定义域限定、值域限定、求关系的定义域和值域等运算来计算切片。该方法避免了构造依赖图的费时费力，降低了出错的机率。 3.进一步拓宽了依赖性分析和Z形式规约切片的应用范围，提出了一种求解提升模式Promote的公式；把定理证明的过程转化为以结论为切片标准的计算一个或多个切片的过程；提出一组针对Z形式规约的耦合性度量准则，考虑了模式修饰、模式包含、模式演算和模式作为类型等多个方面。根据这些度量准则，可以将一些问题发现并杜绝在软件开发的早期阶段，大大减少了由于错误或不合理分析而导致的开销，并可对系统进行有效的评估。