Verification of pointer programs using symbolic method for definite iterations

The symbolic method for verifying definite iterations over hierarchical data structures is extended to allow a restricted change of the structures by the iteration body and exit from the iteration body under a condition. A transformation of definite iterations which use exit from the iteration bodies to the standard definite iterations is justified. Programs over linear lists are considered as a case of study. A technique for proving verification conditions based on both induction principles and notions related to the problem domain is developed. Examples which illustrate application of the symbolic method to pointer program verification are considered.