• 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