Loop Invariants

[timb89]

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! :)

[timb89]

Is the best forum to post this in?

[Stefano Mtangoo]

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

[Narue]

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.