One aspect of comp science that really lets me down is loop invariants.

A question from a past paper that i cant get is to find the loop invariant of the following segment of code:

``````bool linearSearchIter(int a[], int n, int target)
{
int i = 0;
bool found = false;
while (i < n && !found)
{
if (a[i] == target)
found = true;
else
i = i + 1;
}
return found;
}``````

I have found the precondition: a[0...n-1] must be a non empty array, or n >= 1. And the postcondition: Return true if target is true, else false.

Any help would be greatly appreciated! :)

3
Contributors
3
Replies
5
Views
6 Years
Discussion Span
Last Post by Narue

Is the best forum to post this in?

forums are for question to be discussed. so what's your question?

A loop invariant is an assertion that doesn't change between the beginning of the loop and each iteration. In your code, one such assertion is that for any a[x] where x < i, target does not exist. This invariant is true prior to executing the loop because x would be less than 0, which is outside of the bounds of the array. The invariant is true during execution of the loop because you 1) use found as a flag to break the loop when a == target, and 2) do not increment i if target is found. Finally, the invariant is true after the loop because of how the loop is terminated. Either i == n and target does not exist in the entire array, or a is equal to target and target does not exist prior to a (otherwise the loop would have terminated sooner).

``````int i = 0;
bool found = false;
// Invariant (TRUE): -1 is an invalid index
while (i < n && !found)
{
// Invariant (TRUE): The loop breaks without incrementing i when target is found
if (a[i] == target)
found = true;
else
i = i + 1;
}
// Invariant (TRUE): i == n OR a[i] == target``````

Pre and post-conditions are not necessarily invariants, but they can be.