Towards a Transformational Approach to Program Verification

Although most typically used in other contexts, program transformations can simplify program veri-cation by transforming a program containing complex language features into a semantically equivalent program containing only simpler language features. The proof of the transformed program can then be performed using a set of proof rules for only the simpler features. There are tradeoos between the transformational approach and the standard approach to program veriication with regard to proof understandability and compactness of programs and assertions, establishing soundness of the program veriication method, and providing mechanized support for the method. The transformational approach has clear advantages in some of these aspects. This paper illustrates this transformational approach by considering proof rules for escape statements in iterative constructs, and discusses the tradeoos with respect to its use. It also suggests how the approach can be applied to other language constructs, including some involving concurrency, and to solving some problems connected with the development of Hoare axiomatizations.