The Refinement Paradigm: The Interaction of Coding and Efficiency Knowledge in Program Synthesis

A refinement paradigm for implementing a high-level specification in a low-level target language is discussed. In this paradigm, coding and analysis knowledge work together to produce an efficient program in the target language. Since there are many possible implementations for a given specification of a program, searching knowledge is applied to increase the efficiency of the process of finding a good implementation. For example, analysis knowledge is applied to determine upper and lower cost bounds on alternate implementations, and these bounds are used to measure the potential impact of different design decisions and to decide which alternatives should be pursued. In this paper we also describe a particular implementation of this program synthesis paradigm, called PSI/SYN, that has automatically implemented a number of programs in the domain of symbolic processing.