Program Transformations in ASPIK

Abstract

Program transformations need a uniform framework for expressing algorithms as well as algebraic properties. In this paper we present the embedding of program transformations in a software specification system. We demonstrate the methodology by developing a sorting algorithm towards more efficiency, and show how the semantics of the specification Language is the foundation for proving transformation rules correct. We are discussing theoretical aspects - the correctness of transformations – as well as technical issues, e.g. two kinds of user interfaces to a program transformation system.