title: Dafny Loop Invariant might not Hold
body: <p>This is a simple segregating 0s and 1s in the array problem. I can't fathom why the loop invariant does not hold.</p>
  
  <pre><code>method rearrange(arr: array&lt;int&gt;, N: int) returns (front: int)
      requires N == arr.Length
      requires forall i :: 0 &lt;= i &lt; arr.Length ==&gt; arr[i] == 0 || arr[i] == 1
      modifies arr
      ensures 0 &lt;= front &lt;= arr.Length
      ensures forall i :: 0 &lt;= i &lt;= front - 1 ==&gt; arr[i] == 0
      ensures forall j :: front &lt;= j &lt;= N - 1 ==&gt; arr[j] == 1
  {
      front := 0;
      var back := N;
      while(front &lt; back)
          invariant 0 &lt;= front &lt;= back &lt;= N
          invariant forall i :: 0 &lt;= i &lt;= front - 1 ==&gt; arr[i] == 0
          // The first one does not hold, the second one holds though
          invariant forall j :: back &lt;= j &lt; N ==&gt; arr[j] == 1
      {
          if(arr[front] == 1){
              arr[front], arr[back - 1] := arr[back - 1], arr[front];
              back := back - 1;
          }else{
              front := front + 1;
          }
      }
      return front;
  }
  </code></pre>