谓词线性自由程序模式的最小语义保持片的刻画
Characterizing Minimal Semantics-preserving Slices of predicate-linear, Free, Liberal Program Schemas
摘要：
程序模式定义了一类程序，所有程序都具有相同的语句结构，但其功能和谓词可能不同。一个模式因此定义了一个完整的程序类，根据它的符号是如何解释的。模式的子模式是通过删除模式中的某些语句而从模式中获得的。我们证明了给定一个模式$S$，它是谓词线性的，自由的和自由的，使得每个if谓词的真和假部分满足一个简单的附加条件，以及一个切片准则，该切片准则由$S$定义的任何程序执行后给定变量的最终值定义，遵守该切片准则的$S$的最小子模式包含所有函数和谓词符号根据程序切片中的数据依赖关系和控制依赖关系，构造变量所需要的“符号集”，即Weiser的静态切片算法给出的符号集。因此，该算法为满足我们的条件集的模式表示的程序类给出了谓词最小切片。我们还给出了一个例子，以表明相应的结果关于切片的终止行为定义的标准是不正确的。这补充了作者的结果，其中要求$S$为函数线性，而不是谓词线性。
英文摘要：
A program schema defines a class of programs, all of which have identical statement structure, but whose functions and predicates may differ. A schema thus defines an entire class of programs according to how its symbols are interpreted. A subschema of a schema is obtained from a schema by deleting some of its statements. We prove that given a schema $S$ which is predicate-linear, free and liberal, such that the true and false parts of every if predicate satisfy a simple additional condition, and a slicing criterion defined by the final value of a given variable after execution of any program defined by $S$, the minimal subschema of $S$ which respects this slicing criterion contains all the function and predicate symbols `needed' by the variable according to the data dependence and control dependence relations used in program slicing, which is the symbol set given by Weiser's static slicing algorithm. Thus this algorithm gives predicate-minimal slices for classes of programs represented by schemas satisfying our set of conditions. We also give an example to show that the corresponding result with respect to the slicing criterion defined by termination behaviour is incorrect. This complements a result by the authors in which $S$ was required to be function-linear, instead of predicate-linear.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
