English
 
User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Journal Article

On the Mechanical Derivation of Loop Invariants

MPS-Authors
/persons/resource/persons45200

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

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

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
Abstract
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.