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
fDate :
3/1/1981 12:00:00 AM
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;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1981.234517
