On the practicality of Manna's method of verifying the termination and correctness of programs

Program testing or debugging is one of the most time consuming tasks in the development of a computer program; sometimes requiring as much as 90% of the total time [15]. Errors occur in every phase of the development, ranging from errors in the syntax of the programming language (often simply a misplaced comma) to a logical error in the problem specification. Language processors adequately locate and flag the syntax errors; we will not discuss them here. We are much more interested in carefully written programs which are ready for computer testing. Debugging programs exist to aid the programmer in locating infinite loops, printing intermediate results, tracing the sequence of execution, etc., but these can really be considered computer-assisted console debugging procedures. In a batch environment, the use of these techniques requires foresight as to what might go wrong as the requests are made prior to execution; it is not always easy to locate the proper check points, nor is it easy to know what information to request. A general procedure followed in program testing is to apply a set of simple test data to the program and to use hand calculations to check the results. The selection of this set of test data is often a non-trivial problem. Further, a successful run does not guarantee that the program will terminate and give correct results for all values of the input data. All possible branches in the program should be checked with a variety of data. For larger programs, thorough testing of every branch is impractical, if not impossible. It is quite common to find that a "proven" program will run successfully many times and then suddenly fail for a given input. A program is rarely known to e absolutely correct. For this reason program maintenance continues to consume a great deal of programmer and computer time. Clearly, a method of proving the termination and correctness of programs would be desirable. We would like a program which would accept as input the program to be tested and its specifications, and which would determine if, for all inputs: 1) The program terminates and delivers correct results, 2) The program terminates, but delivers incorrect results, 3) The program terminates, but delivers no results, or 4) The program does not terminate. Ideally this program would also, in the case of error, locate the offending portion of the program. We would further require that the computer time required for this procedure be reasonable. The porribilitY of the development of such a verifying program is suggested by the work of Manna [9, 10] in which he relates the problems of termination and correctness of programs to equivalent problems in first-order logic. He has translated the question of the termination and correctness of programs into the question of the satisfiability of formulas of the first-order predicate claculus (or, equivalently, the validity). He has described an algorithm, which will construct, for a given program (whose syntax and - notion of execution (semantics) has been defined) or abstract program, a first-order formula characterizing its execution. He shows that the problem of proving the termination and correctness of the program or abstract program is equivalent to proving the validity of the formula. The validity problem is undecidable. However, it is semi decidable. (There are subclasses of formulas for which validity is decidable and Manna shows that there exist subclasses of abstract programs, which are subclasses of formulas.) Any decision or semi decision procedure that applies to formulas in first-order logic can be applied to prove the termination and correctness of programs and abstract Programs. One such procedure is based on the resolution principle [11, 131]. The Purpose of this essay is to examine the practicality of this method for proving the termination and correctness of programs by determining the ease of constructing the first-order formula and the applicability of a semi decision procedure to this formula. Because a large number of "tested" Fortran programs in varying degrees of complexity were readily available, Fortran was selected as the programming language. By 11tested", we mean simply that the programs terminated and gave correct results for one or more sets of input data. Resolution was selected as the semi decision procedure because it is machine-oriented and programs equivalent to the decidable utilizing this principle exist. The discussion is limited to the termination problem of programs. Manna has extended his results to include correctness and equivalence; he claims that they are -reducible to the termination problem. The programs considered are limited to simple iterative programs written in Fortran. To make this paper self-contained, Chapter II contains the description of a first-order predicate calculus and a description of Robinson's resolution procedure [11, 131]. Chapter III contains a summary of Manna's work, his principal definitions and theorems [9]. If the resolution procedure is to be applicable, the time required to reach a solution must be reasonable; in general, this cannot be determined from the formula itself. However, the first level of the procedure is to obtain all possible resolvents from the original set of clauses, making no substitutions for individual variables. The number of steps of resolution required for this first level is determined by the number of pairs of matching complementary literals contained in the original set of clauses. This provides a first estimate on the amount of time required. The minimum number of steps will be taken if the empty clause is a member of the set of first resolvents. The time required to obtain this set of first resolvents is therefore among the first factors used in evaluating the practicality of this method of verifying the termination of programs. In Chapter IV a Fortran program is examined in detail; rules for constructing the graph of the program from the Fortran source statements are presented. An algorithm to count the number of matching complementary literals appearing in the formula of a program without constructing the actual program is presented. A number of Fortran programs were then examined; the number of steps of resolution required for the first level was determined for each program. In all cases the number of steps and therefore the time required is reasonable. However, it is shown that, except for exactly one program, a solution in this first level is not possible (i.e., the empty clause will not be the resolvent of two original clauses). The question of the applicability of resolution to these formulas is not fully answered; additional information is required. An experiment to study the problem further and to collect the necessary data is described.Technical report dcs-tr-1