How do we define a loop invariant?

Question

We know that a loop variant is defined as a statement that is true before and after every iteration of the loop. But is that definition too loose? Let us look at a concrete example: linear search.

Input: A sequence of n numbers A = (a₁, a₂, a₃, ..., a_n) and a value v

Output: An index i such that v = A[i] or NIL if v is not found in A

Here is my pseudocode:

linear_search(A, v)
1 for i ∈ {1, 2, ..., n}
2     if A[i] = v
3         return i
4 return NIL

So a typical loop invariant would be that (since we are searching from left to right) v is not on the left side of the current index, or mathematically, P: ∀p ∈ {1, 2, ..., i - 1}, A[p] ≠ v. This is clearly true, even at the start because p ∈ Ø is false, which makes P true, remembering that every universally quantified statement can be thought of as a conditional statement. (But it is easier to think of it informally: at the start, there is nothing on the left side of v.)

We could also use a conditional statement that is less restricting. In this case, Q: If A[i] = v, then 1 ≤ i ≤ n. Obviously, this is true if v is found. If v is not found, A[i] = v is false and Q becomes true regardless of the value of i. Q is also true if we change our algorithm to search from right to left.

Maybe we want to be less restricting than that. What about using a statement that is always true? R: Either A[i] = v or A[i] ≠ v. R holds before and after every iteration of the loop.

Which of the statements P, Q and R are valid to use as a loop invariant?

A loop invariant should be a 'useful' property of the loop itself. Your property R is more of a tautology irrespective of the loop. So IMO only P and Q can be thought of as loop invariants although Q is weaker. — Abhishek Bansal, Nov 10 '16 at 04:18
I highly recommend David Gries, The Science of Programming, which gives a methodical development of this topic and much more. — Gene, Nov 10 '16 at 04:19
a possible duplicate of - http://stackoverflow.com/questions/3221577/what-is-a-loop-invariant — Subham Tripathi, Nov 10 '16 at 05:17

Matt Timmermans · Accepted Answer · 2016-11-10T05:23:51.897

What do you want a loop invariant for? Maybe you want to prove that your algorithm is correct, i.e., that:

linear_search(A,v) = i ⇒ A[i] = v

and

linear_search(A,v) = NIL ⇒ v ∉ A

The first one is easy. To prove the second one, you can make use of your loop invariant P. Since it was true for i=n if the function returns NIL, you have

linear_search(A,v) = NIL
⇒ ∀p ∈ {1, 2, ..., n}, A[p] ≠ v
⇒ v ∉ A

Your candidate P is useful for this purpose, and the others are not.

Also, you can't just pick a loop invariant -- you have to prove it in order to prove your algorithm is correct. The iterative nature of loops lends itself to proof by induction, and invariants like your candidate P are easy to prove that way.

How do we define a loop invariant?

1 Answers1