Computer-Aided Computing

PVS is a highly automated framework for speci cation and veri cation. We show how the language and deduction features of PVS can be used to formalize, mechanize, and apply some useful program transformation techniques. We examine two such examples in detail. The rst is a fusion theorem due to Bird where the composition of a catamorphism (a recursive operation on the structure of a datatype) and an anamorphism (an operation that constructs instances of the datatype) is fused to eliminate the intermediate data structure. The second example is Wand's continuation-based transformation technique for deriving tail-recursive functions from non-tail-recursive ones. These examples illustrate the utility of the language and inference features of PVS in capturing these transformations in a simple, general, and useful form.

• Type: Conference
• Year: 1995
• Where: MPC
• Authors: Natarajan Shankar
• Keywords: Mathematics, MPC 1995, Transformation Technique, Useful Program Transformation, Veri Cation