SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Steps Towards Mechanizing Program Transformations Using PVS
 by Dr. Natarajan Shankar.

Appears in Science of Computer Programming, Volume 26, Number 1-3.
Pages 33–57.

PVS is a highly automated framework for specification and verification. We show how the language and deduction features of PVS can be used to formalize, mechanze, and apply some useful program transformation techniques. We examine two such examples in detail. The first is a fusion theorem due to Bird where the coposition 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.
BibTEX Entry
    AUTHOR = {{N.} Shankar},
    TITLE = {Steps Towards Mechanizing Program Transformations Using {PVS}},
    JOURNAL = {Science of Computer Programming},
    VOLUME = {26},
    NUMBER = {1--3},
    YEAR = {1996},
    PAGES = {33--57},
    URL = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy