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?