Abstract

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.

File
Issue
Pages
103-123