This Article 
 Bibliographic References 
 Add to: 
Verifying Definite Iteration Over Data Structures
June 1995 (vol. 21 no. 6)
pp. 506-514
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.

[1] S.K. Basu and J. Misra,“Proving loop programs,” IEEE Trans. on Software Engineering, vol. 1, no. 1, pp. 76-86, Mar. 1975.
[2] S.K. Basu and J. Misra,“Some classes of naturally provable programs,” Proc. 2nd Int’l Conf. on Software Engineering, pp. 400-406.Washington, D.C.: IEEE Computer Society Press, 1976.
[3] W.S. Brainerd and L.H. Landweber,Theory of Computation.New York: John Wiley&Sons, 1974.
[4] D.D. Dunlop and V.R. Basili,“A comparative analysis of functional correctness,” Computing Surveys, vol. 14, no. 2, pp. 229-244, June 1982.
[5] D.D. Dunlop and V.R. Basili,“Generalizing specifications for uniformly implemented loops,” ACM Trans. on Programming Languages and Systems, vol. 7, no. 1, pp. 137-158, Jan. 1985.
[6] R.E. Griswold and M.T. Griswold,The Icon Programming Language, 2nd ed. Englewood Cliffs, N.J.: Prentice-Hall, 1990.
[7] C.A.R. Hoare, "An Axiomatic Basis for Computer Programming," Comm. ACM, 1969.
[8] C.A.R. Hoare,“A note on the FOR statement,” BIT, vol. 12, pp. 334-341, 1972.
[9] B.W. Kernighan and D.M. Ritchie, The C Programming Language.Englewood Cliffs, N.J.: Prentice Hall, 1978.
[10] R. Linger, H. Mills, and B. Witt, Structured Programming: Theory and Practice. Addison-Wesley Publishing Co., 1979.
[11] J. Kittler and J. Foglein, "On Compatibility and Support Functions in Probabilistic Relaxation," Computer. Vision, Graphics, and Image Processing, 1986.
[12] B. Liskov and J. Guttag, Abstraction and Specification in Program Development. MIT Press, 1986.
[13] Harlan D. Mills, "The New Math of Computer Programming," Comm. of the ACM, vol. 18, p. 44, Jan. 1975.
[14] H.D. Mills,M. Dyer,, and R.C. Linger,“Cleanroom software engineering,” IEEE Software, vol. 4, no. 5, pp. 19-24, Sept. 1987.
[15] J. Misra,“Some aspects of the verification of loop computations,” IEEE Trans. on Software Engineering, vol. 4, no. 6, pp. 478-486, Nov. 1978.
[16] R. W. Selby, V. R. Basili, and F. T. Baker,“Cleanroom software development: An empirical investigation,”IEEE Trans. Software Eng., vol. SE-13, pp. 1027–1037, Sept. 1987.
[17] M. Shaw, W. Wulf, and R. London, "Abstraction and Verification in Alphard: Defining and Specifying Iterators and Generators," Comm. ACM, vol. 20, no. 9, pp. 553-564, Aug. 1977.
[18] J.T. Schwartz et al., Programming with Sets: An Introduction to SETL, Springer, Berlin, 1986.
[19] A.M. Stavely,“An empirical study of iteration in applications software,” J. of Systems and Software, vol. 22, pp. 167-177, Sept. 1993.

Index Terms:
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. 6, pp. 506-514, June 1995, doi:10.1109/32.391377
Usage of this product signifies your acceptance of the Terms of Use.