| | | Projects |
As a result of our work in program slicing, we found that program schema theory enabled them to precisely express the problems that we were tackling; namely the existence of statement minimal slicing algorithms at the `dataflow' level of abstraction. For such problems a class of schema which we 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. We 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. We hope that our 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.
| | | Projects |