STEPS TOWARDS MECHANIZING PROGRAM TRANSFORMATIONS USING PVS

PVS is a highly automated framework for specification and verification . We show how the language and deduction features of PVS can be used t o formalize, mechanize, and apply some useful program transformation t echniques, We examine two such examples in detail. The first is a fusi on theorem due to Bird where the composition of a catamorphism (a recu rsive operation on the structure of a datatype) and an anamorphism (an operation that constructs instances of the datatype) are fused to eli minate the intermediate data structure. The second example is Wand's c ontinuation-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 th ese transformations in a simple, general, and useful form.