Linear Schemas for Program Dependence

点击翻译按钮获取中文摘要

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.