We aim to specify program transformations in a declarative style,
and then to generate executable program transformers from such
specifications. Many transformations require non-trivial program
analysis to check their applicability, and it is prohibitively
expensive to re-run such analyses after each transformation. It is
desirable, therefore, that the analysis information is incrementally
updated.
We achieve this by drawing on two pieces of previous work:
first, Bernhard Steffen's proposal to use model checking
for certain analysis problems, and second, John Conway's theory of
language factors. The first allows the neat specification of
transformations, while the second opens the way for an incremental
implementation. The two ideas are linked by using regular
patterns instead of Steffen's modal logic: these patterns can
be viewed as queries on the set of program paths.
