Linear Schemas for Program Dependence

程序依赖性的线性模式

• 批准号: EP/E002919/1
• 负责人: S Danicic
• 金额: $ 38.41万
• 依托单位: Goldsmiths University of London
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2006
• 资助国家: 英国
• 起止时间: 2006 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FE002919%2F1
• 关键词: Linear; Schemas; 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.

程序模式是一种表示具有相同语法结构的无限计算机程序集的符号。如果一个程序模式的一个性质可以被证明，那么这个性质对于这个模式所表示的无限程序集合中的每一个程序都成立。推理与模式，因此，一个非常强大的mechanism.As他们的工作在程序切片，proposers发现，程序模式理论使他们能够精确地表达的问题，他们正在处理，即存在的语句最小切片算法在"低“抽象层次。对于这样的问题一类模式，他们称之为“线性模式”的介绍。线性模式是一个没有谓词或函数符号出现超过一次的模式。偶然的是，提出者后来发现线性条件有助于证明模式等价的可判定性。等价的判定性是自动检查两个不同模式是否表示同一类模式的能力。他们证明了保守的、自由的、线性模式的等价是可判定的，后来又通过证明自由的、自由的线性模式的等价是在多项式时间内可判定的来加强这一点。这项工作代表了图式理论在中断了大约30年之后取得的重大进展。有强有力的证据表明，这种额外的，但自然的条件的线性（或部分形式的线性）将导致进一步的可判定性结果的理论schema.The提议者希望他们的新结果将导致重新评估的大量工作在程序模式理论，并进一步研究其应用在现代框架。许多静态程序转换和分析，实际上所有使用数据和控制流的分析，都发生在抽象的模式级别。这意味着对一个程序的分析将为它的模式等价类中的所有程序产生相同的结果。这项研究的一个重要组成部分将是进一步调查在何种程度上大量的工作理论的模式是有关切片特别是和其他形式的静态程序分析和转换一般。