AbstractWe present an extension of the Lübeck Transformation System LTS automating the fusion of a function with a catamorphism as a refinement step in algebraic program development. The system detects catamorphisms in constructor-based higher-order algebraic specifications and generates an axiomatisation of the composition function. As the basis we give a generalized treatment of the fusion theorem in the setting of algebraic specifications. We illustrate the approach presenting compound fusion transformations for non-free data structures.
Categories and Subject Descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs; I.2.2 [Artificial Intelligence]: Automatic Programming
Additional Key Words and Phrases: computer aided programming, program transformation, higher-order algebraic specification, catamorphism, fusion
Selected references
- R. M. Burstall and John Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44-67, January 1977.
- Karl Meinke. Universal algebra in higher types. Theoretical Computer Science, 100(2):385-417, 29 June 1992.
- Alberto Pettorossi and Maurizio Proietti. Rules and strategies for transforming functional and logic programs. ACM Computing Surveys, 28(2):360-414, June 1996.