On Development of Iterative Programs from Function Specifications

A systematic approach to the development of totally correct iterative programs is investigated for the class of accumulation problems. In these problems, the required output information is usually obtained by accumulation during successive passes over input data structures. The development of iterative programs for accumulation problems is shown to involve successive generalizations of the data domain and the corresponding function specifications. The problem of locating these generalizations is discussed. It is shown that not all function specifications can be realized in terms of terminating computations of a stand-alone iterative program. A linear data domain is defined in terms of decomposition and finiteness axioms, and the property of well behavedness of a loop body over a linear data domain is introduced. It is shown that this property can be used to generate loop body specifications from specifically chosen examples of program behavior. An abstract program for an accumulation problem is developed using these considerations. The role of generalizations as an added parameter to the program development process is discussed.