Program Transformation using Temproal Logic Specifications

This thesis describes a specification language for program transformations as well as how to implement these transformations and formally analyse them. The unusual feature of this language is that the applicability conditions of the transformations are expressed using a form of temporal logic. The aim of the language is to provide easy and flexible specifications of program transformations. The thesis provides the following contributions:

• A specification language for transformations (TRANS) is introduced that combines elements of rewriting, temporal logic and logic programming. Several examples are presented to show the flexibility of the language in specifying many common transformations found in optimising compilers.
• It is shown how this language could be used in a development tool to improve the efficiency of a program. As a proof of concept, an implementation is described and proved correct. This implementation shows that any transformation specified in TRANS can be automatically executed.
• It is shown how correct implementations can also be derived for languages with complex features without having to change the transformation specifications. Example languages are considered with unknown code fragments, aliasing and procedure calls.
• A method is presented to prove that transformations do not change the output behaviour of the programs they transform. This is illustrated with three example proofs of correctness.
• The issue of disabling interference (when one transformation will cause another not to apply) is discussed and it is shown that for a certain sub-class of transformation specifications the question of whether two transformations exhibit this interference is decidable.