Title :
Verifying definite iteration over data structures
Author :
Stavely, Allan M.
Author_Institution :
Dept. of Comput. Sci., New Mexico Techl., Socorro, NM, USA
fDate :
6/1/1995 12:00:00 AM
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
Keywords :
data structures; formal specification; iterative methods; program control structures; program verification; data structures; data-structure access; data-structure termination; definite iteration; functional specifications; functional style; program verification; programming language constructs; structured programming; verification; Computer languages; Data structures; Functional programming; Milling machines; Programming profession;
Journal_Title :
Software Engineering, IEEE Transactions on
