DocumentCode
798367
Title
Verifying definite iteration over data structures
Author
Stavely, Allan M.
Author_Institution
Dept. of Comput. Sci., New Mexico Techl., Socorro, NM, USA
Volume
21
Issue
6
fYear
1995
fDate
6/1/1995 12:00:00 AM
Firstpage
506
Lastpage
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
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;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/32.391377
Filename
391377
Link To Document