Symbolic verification method for definite iterations over tuples of data structures

The symbolic method for verifying definite iterations over hierarchical data structures is extended to allow tuples of data structures and exit from the iteration body under a condition. Transformations of these generalized iterations to the standard ones are proposed and justified. Useful properties of the transformations are given. A technique for generating verification conditions and their proving, including induction principles, is described. For iterations over files, a problem-oriented proving technique is presented too. Examples which illustrate application of the symbolic method to file program verification are considered.