DocumentCode
752245
Title
The Determination of Loop Invariants for Programs with Arrays
Author
Ellozy, Hamed A.
Author_Institution
Computer Sciences Department, IBM Thomas J. Watson Research Center
Issue
2
fYear
1981
fDate
3/1/1981 12:00:00 AM
Firstpage
197
Lastpage
206
Abstract
This paper describes a method for the generation of loop predicates (or invariant assertions) for programs operating on arrays. The technique described is an application of difference equations.
Keywords
Difference equations; inductive assertions; invariant assertions; loop predicates; program validation; Control systems; Counting circuits; Difference equations; Flowcharts; Input variables; Terminology; Difference equations; inductive assertions; invariant assertions; loop predicates; program validation;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/TSE.1981.234517
Filename
1702826
Link To Document