title: Loop invariant proof understanding
body: <p>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:</p>
  
  <pre><code>/* 0 ≤ m &lt; n &lt; ASIZE AND A[m] ≥ A[m+1] ≥ ... ≥ A[n] */
  void ReverseArray(int A[], int m, int n)
  {
    int temp;
    while (m &lt; n)
    {
          temp = A[m]; A[m] = A[n]; A[n] = temp;
          m++;
          n--;
          /* loop invariant: 0 &lt; m &lt; n &lt; ASIZE OR m == n OR m == n+1 */
  } 
  }
  /* for the initial values of m and n, A[m] ≤ A[m+1] ≤ ... ≤ A[n] */
  </code></pre>
  
  <p>The loop invariant is: 0 &lt; m &lt; n &lt; ASIZE OR m == n OR m == n+1</p>
  
  <p>I think I understand the 0 &lt; m &lt; n &lt; 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.</p>
  
  <p>But I do not understand why m == n and m == n+1.</p>
  
  <p>Any thoughts?</p>