Linear Schemas for Program Dependence

程序模式是一种表示具有相同句法结构的无限计算机程序集的符号。如果可以证明程序模式的一个性质，则该性质将对由该模式表示的无限程序集中的每个程序都成立。因此，用模式进行推理是一种非常强大的机制。由于他们在程序切片方面所做的工作，提出者发现程序图式理论使他们能够准确地表达他们正在处理的问题，即在抽象的数据流级别上存在语句最小切片算法。对于这类问题，引入了一类他们称之为“线性模式”的模式。线性模式是指没有谓词或函数符号出现多次的模式。巧合的是，后来的提出者发现，线性条件有助于证明模式等价的可判定性。等价的可判断性是自动检查两个不同的模式是否代表同一类模式的能力。他们证明了保守、自由、线性模式的等价性是可判定的，后来通过证明自由、自由、线性模式的等价性在多项式时间内是可判定的，从而加强了这一点。这项工作标志着图式理论在中断了约30年后取得了重大进展。有强有力的证据表明，施加这种额外但自然的线性条件(或部分线性形式)将导致图式理论中进一步的可判定性结果。提出者希望他们的新结果将导致对程序图式理论中大量工作的重新评价，并进一步研究其在现代框架中的应用。这是本研究提出的主要动机之一。大多数静态程序转换和分析，实际上所有使用数据和控制流的分析都发生在抽象的图式级别。这意味着对程序的分析将为其模式等价类中的所有程序产生相同的结果。这项研究的一个重要部分将是进一步调查模式理论的大量工作在多大程度上与切片以及一般的其他形式的静态程序分析和转换相关。

Program schemas are a notation for representing an infinite set of computer programs all with the same syntactic structure. If a property of a program schema can be proved, this property will hold for every program in the infinite set of programs represented by the schema. Reasoning with schemas is, thus, a very powerful mechanism.As a result of their work in program slicing, the proposers found that program schema theory enabled them to precisely express the problems that they were tackling; namely the existence of statement minimal slicing algorithms at the `dataflow' level of abstraction. For such problems a class of schema which they called a `linear schema' was introduced. A linear schema is one in which no predicate or function symbol occurs more than once.Serendipitously, the proposers later discovered that the linearity condition helped in proving decidability of equivalence of schemas. Decidability of equivalence is the ability to automatically check whether two different schemas represent the same class of schemas. They proved that equivalence of conservative, free, linear schemas is decidable and later strengthened this by proving that equivalence of liberal, free linear schemas is decidable in polynomial time. This work represented significant progress in the field of schema theory after a hiatus of about thirty years. There is strong evidence that the imposition of this extra but natural condition of linearity (or partial forms of linearity) will lead to further decidability results in the theory of schemas.The proposers hope that their new results will lead to a re-appraisal of the substantial body of work in program schema theory and to further research its applications in a modern framework. This is one of the main motivations of this research proposal.Much static program transformation and analysis, in fact all analysis which uses data and control flow, takes place at the schema level of abstraction. This means the analysis of a program will produce the same results for all programs in its schema equivalence class. An important part of this research will be to investigate further the extent to which the large body of work on the theory of schemas is relevant to slicing in particular and to other forms of static program analysis and transformation in general.