A Logic Foundation for Program Transformations

Abstract. This paper presents a uniform foundation for representing, analysing and transforming programs and models. It is firmly grounded on logic and defines a seamless integration of declarative analyses and of transformations based on these analyses. As such it is an entirely novel approach that recommends itself as an alternative to known transformation formalisms and possibly a unifying framework for previously disparate work on analysis and transformation of programs or models. The paper introduces a representation of models and programs as a set of ground logic facts, defines the notion of conditional transformations (CTs) and two different semantic variations of CT sequences. The semantics of CTs and CT sequences is defined leveraging on the declarative semantics of logic programs for the interpretation of conditions and expressing model transformations by transformation of logic programs.