The Determination of Loop Invariants for Programs with Arrays

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. Copyright © 1981 by The Institute of Electrical and Electronics Engineers, Inc.