Symbolic Method of Verification of Definite Iterations over Altered Data Structures

摘要

To extend the application domain of the symbolic verification method, definite iterations over altered data structures, which are found to reduce to standard finite iterations, are introduced. The suggested reduction is applicable to definite iterations over altered data structures that contain an exit statement by a condition depending on the variables modified by the loop body. The suggested generalization of the symbolic method makes it applicable to verifying programs over pointers. To illustrate the discussion, the verification of two programs designed for processing linear lists—searching for an element with reordering and elimination of zero elements—is described.