CODEWITHSUNDEEP
cloopsloop-invariant
user081608
user081608

Reputation: 1113

Loop invariant proof understanding

I am trying to learn about loop invariants in C. I have a code and I have the loop invariant but I do not fully understand why. Here is the code:

/* 0 ≤ m < n < ASIZE AND A[m] ≥ A[m+1] ≥ ... ≥ A[n] */
void ReverseArray(int A[], int m, int n)
{
  int temp;
  while (m < n)
  {
        temp = A[m]; A[m] = A[n]; A[n] = temp;
        m++;
        n--;
        /* loop invariant: 0 < m < n < ASIZE OR m == n OR m == n+1 */
} 
}
/* for the initial values of m and n, A[m] ≤ A[m+1] ≤ ... ≤ A[n] */

The loop invariant is: 0 < m < n < ASIZE OR m == n OR m == n+1

I think I understand the 0 < m < n < ASIZE. It would be because of the while loop and it says that m cant be 0 but it has to be less than n. And n has to be smaller than the array size.

But I do not understand why m == n and m == n+1.

Any thoughts?

Upvotes: 2

Views: 393

Answers (3)

jxh
jxh

Reputation: 70412

If before the loop body, it was the case that m + 1 == n, then at the end of the loop, m will have been incremented and n will have been decremented. At that point, m == n + 1.

For example, when m has the value 2, and n has the value 3. Then after m++; n--;, m has the value 3 and n has the value 2.

If before the loop body, it was the case that m + 2 == n, then after the loop body, m == n. For example if m has the value 2 and n has the value 4, then afterwards, m is 3 and n is 3.

For either of the cases where after the loop body the result is m == n or m == n + 1, the loop control will be false, and so that case will cause the loop to stop.

Upvotes: 1

Maja Piechotka
Maja Piechotka

Reputation: 7216

Write down 2 cases of procedure - for even and odd length of array. For example create a table with number of iteration, array and values of m and n before itera. I believe it would be simplest to do it on your own and proceed by code line by line (table itself might not be so helpful in understanding the whole problem as doing it).

PS. The invariant seems to be too weak to establish the postcondition.

Upvotes: 1

Daniel Daranas
Daniel Daranas

Reputation: 22624

But I do not understand why m == n and m == n+1.

At the point were the loop invariant is located, this expression (the loop invariant) is guaranteed to be true:

0 < m < n < ASIZE OR m == n OR m == n+1

However, this (the "part that you understand") is not always true:

0 < m < n < ASIZE

Why? Because m is incremented, n is decremented, hence m < n may not be true anymore.

That's why you need to "amplify" the loop invariant so that it is always true, including these cases, m == n and m == n+1, which may arise during the normal execution of the loop.

So if you said that the invariant is just the "part that you understand", you would be wrong - your loop invariant would fail, which is (by definition) a no-no.

Upvotes: 1

Related Questions