User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Journal Article

On the Mechanical Derivation of Loop Invariants


Plaisted,  David
Programming Logics, MPI for Informatics, Max Planck Society;

External Ressource
No external resources are shared
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available

Chadha, R., & Plaisted, D. (1993). On the Mechanical Derivation of Loop Invariants. Journal of Symbolic Computation, 15(5/6), 705-744.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0023-C745-8
We describe an iterative algorithm for mechanically deriving loop invariants \u000Afor the purpose of proving the partial correctness of programs. The algorithm \u000Ais based on resolution and a novel unskolemization technique for deriving \u000Alogical consequences of first‐order formulas. Our method is complete in the \u000Asense that if a loop invariant exists for a loop in a given first‐order \u000Alanguage relative to a given finite set of first‐order axioms, then the \u000Aalgorithm produces a loop invariant for that loop which can be used for proving \u000Athe partial correctness of the program. Existing techniques in the literature \u000Aare not complete.