非表示:
キーワード:
-
要旨:
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.
