A simple calculus for program transformation (inclusive of induction)

AbstractA basic purpose of transformation systems is the application of ‘correctness-preserving rules’ in order to derive from given programs new, ‘equivalent’ ones. An important aspect here is the usage of induction principles, without which transformation systems would have too limited power.The paper presents a formal system of ‘transformation rules’ that incorporates induction. This system is a kind of ‘Gentzen-style calculus’, impoverished, however, to a degree that just meets the needs of program transformation. Thus we achieve a basis for the design of transformation systems, which is both simple and sound