Expression Procedures and Program Derivation.
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
We explore techniques for systematically deriving programs from specifications. The goal of this exploration is a better understanding of the development of algorithms. Thus, the intention is not to develop a theory of programs, concerned with the analysis of existing programs, but instead to develop a theory of programming, dealing with the process of constructing new programs. Such a theory would have practical benefits both for programming methodology and for automatic program synthesis. We investigate the derivation of programs by program transformation techniques. By expanding an ordinary language of recursion equations to include a generalized procedure construct the expression procedure, our ability to manipulate programs in that language is greatly facilitated. The expression procedure provides a means of expressing information not just about the properties of individual program elements, but also about the way they relate to each other. A set of three operations -- abstraction, application, and composition -- for transforming programs in this extended language is presented. We prove using operational semantics that these operations preserve the strong equivalence of programs. The well-known systems of Burstall and Darlington and of Manna and Waldinger are both based on an underlying rule system that does not have this property.
- Theoretical Mathematics