# Finding a good loop invariant

I want to prove that the following program is correct. The code takes an array i of length N and a number x. At the end, the value of found should be true if the array contains x and false otherwise.

found := false;
i := 0 ;
while i < N do {
found := found || (a[i]=x);
i:=i+1
}

The given preconditions are that N >= 0 and that the array is sorted in ascending order (however, I don't know how the fact that it is sorted can help).

As postcondition, I think the following would suffice: the value of found equals the value of the predicate “there exists an i in the range [0, N) such that a[i] == x

However, I am stuck at this point and don't know how to continue. I cannot think of any loop invariant that has any relation to the postcondition. What would you suggest as a loop invariant?

• The method of weakest precondition is sometimes helpful in these kind of cases.
– Juho
Jun 11, 2015 at 13:36
• this might help: cs.stackexchange.com/questions/54954/… Apr 7, 2016 at 17:19

So we're interested in the following property: “the value of found equals the value of the predicate there exists a $k$ in the range $[0, i)$ such that $a[k] = x$”. Note that I use a name other than i for the existential variable, since i is now used in the context. The quantifier pile-up is:
there exists an index $k$ such that …