Issue No. 06 - June (1995 vol. 21)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.391377
Methods are presented for verifying loops which iterate over elements of data structures. This verification is done in the functional style developed by Mills and others, in which code is verified against the function that the code is intended to compute. The methods allow the verifier to concentrate on the essential computation performed on each element of the structure, and separate out such concerns as data-structure access and termination so that they do not need to be verified again for every loop in the program. The methods are applicable to a large class of data structures and iterations over them.
Data structures, functional specifications, program verification, programming language constructs, structured programming.
Allan M. Stavely, "Verifying Definite Iteration Over Data Structures", IEEE Transactions on Software Engineering, vol. 21, no. , pp. 506-514, June 1995, doi:10.1109/32.391377