An Extension of the Direct Method for Verifying Programs

A direct method based on a finite set of path formulas which describe the input-output relations of a given program can be used to verify programs containing no overlapping loops. One major difficulty in verifying programs with overlapping loops using the above method is that too many path formulas (possibly infinite) needed to be considered. In this paper, we circumvent the above difficulty by applying the concept of modularity. The idea is to divide a program with overlapping loops into several small modules so that each module contains no overlapping loop. This can always be achieved if the program is in structured form. Then the path formulas will be derived for each module. By combining the path formulas for the modules, one can further obtain the path formulas for the given program and then use them to verify the program.