One of the principal impediments to widespread use of automated program verification methodology is due to the user burden of creating appropriate inductive assertions. In this paper, we investigate a class of programs for which such inductive assertions can be mechanically generated from Input-output specifications. This class of programs, called accumulating programs, are iterative realizations of problems in which the required output information is accumulated during successive passes over the input data structures. Obtaining invariant assertions for such programs is shown to be equivalent to the problem of generalizations of specifications to that over an extended closed data domain. For this purpose, a set of basis data elements are to be conceived of as generating the extended domain. An arbitary data element would thus be considered as uniquely decomposable into a sequence of basis elements. The structural relations between the components of a data element are used to extend program behavior and thus obtain the desired invariant.

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.

Given a `DO WHILE' programPand a functionFon a domainD, the authors investigate the problem of proving (or disproving) ifPcomputesFoverD. It is shown that ifPsatisfies certain natural constraints (well behaved), then there is a loop assertion independent of the structure of the loop body, that is both necessary and sufficient for proving the hypothesis. These results are extended to classes of loop programs which are not well behaved and to FOR loops. The sufficiency of Hoare's DO WHILE axiom for well-behaved loop programs is shown. Applications of these ideas to the problem of mechanical generation of assertions is discussed.

The authors investigate the strong verification of programs using the concept of predicate transformer introduced by Dijkstra (1974). They show that every do-while program has a loop invariant that is both necessary and sufficient proving strong verification. This loop invariant is shown to be the least fixpoint of a recursive function mapping predicates to predicates that is defined by the program and the postcondition.

The complexity closure of a computable function is defined by a set of axioms. The axioms are satisfied by complexity classes that are computation time closed and also by other complexity classes which do not have this property. It is then shown that there exist honest recursive functions whose complexity closure are setwise incomparable. Further that there exist chains of honest recursive functions whose complexity closures are densely ordered under set inclusion.