The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - June (1995 vol.21)
pp: 506-514
ABSTRACT
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.
INDEX TERMS
Data structures, functional specifications, program verification, programming language constructs, structured programming.
CITATION
Allan M. Stavely, "Verifying Definite Iteration Over Data Structures", IEEE Transactions on Software Engineering, vol.21, no. 6, pp. 506-514, June 1995, doi:10.1109/32.391377
5 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool