title: What is the wrong with my code in dafny?
body: <p>I try to use dafny to verify the correctness with my qsort function, but idk why there are verified failures about my code. 
  Here is my code:   </p>
  
  <pre><code>    method Testing (a: array&lt;int&gt;)
        requires  a.Length &gt; 0
        modifies a
      {
          qsort(a,0,a.Length-1);
          var i :int := 0;
          while(i&lt;a.Length-1)
            decreases a.Length - 1 - i
          {
            assert a[i] &lt;= a[i+1];
            i := i+1;
          }
      }
      method qsort(a: array&lt;int&gt;,left: int,right: int)
          requires left&gt;=0 &amp;&amp; right &lt; a.Length
          modifies a
          decreases right - left
      {
        if (right &gt; left)
        {
            var pivotValue: int := a[left];
            var t: int := a[left];
            a[left] := a[right-1];
            a[right-1] := t;
            var storeIndex: int := left;
            var i :int := left;
            while i &lt; right - 1
              invariant left &lt;= storeIndex &lt; right
              decreases right - i
            {
                if a[i] &lt; pivotValue
                {
                  t := a[storeIndex];
                  a[storeIndex] := a[i];
                  a[i] := t;
                  storeIndex := storeIndex+1;
                }
                i := i+1;
            }
            t := a[right-1];
            a[right-1] := a[storeIndex];
            a[storeIndex] := t;
            qsort(a,left,storeIndex);
            qsort(a,storeIndex+1,right);
        }  
      }
  </code></pre>
  
  <p>The errors are:</p>
  
  <ol>
  <li><p>assertion violation</p>
  
  <pre><code>assert a[i] &lt;= a[i+1];
  </code></pre></li>
  <li><p>This loop invariant might not be maintained by the loop. </p>
  
  <pre><code>invariant left &lt;= storeIndex &lt; right + 1
  </code></pre></li>
  <li><p>failure to decrease termination measure</p>
  
  <pre><code>qsort(a,left,storeIndex);
  </code></pre>
  
  <p>Thanks to the answer from @James Wilcox, I rewrote my code as:</p>
  
  <pre><code>method qsort(a: array&lt;int&gt;,left: int,right: int)
  requires left&gt;=0 &amp;&amp; right &lt;= a.Length
  ensures (exists p | left&lt;=p&lt;right :: (forall k: int :: left &lt; k &lt; p ==&gt; a[k] &lt;= a[p]) &amp;&amp; (forall j: int :: p &lt; j &lt; right ==&gt; a[j] &gt;= a[p]))
  modifies a
  decreases right - left
  {
    if (right &gt; left)
    {
        var pivotValue: int := a[left];
        var t: int := a[left];
        a[left] := a[right-1];
        a[right-1] := t;
        var storeIndex: int := left;
        var i :int := left;
        while i &lt; right - 1
          invariant left &lt;= storeIndex &lt; right
          invariant storeIndex &lt;= i
          decreases right - i
        {
            if a[i] &lt; pivotValue
            {
              t := a[storeIndex];
              a[storeIndex] := a[i];
              a[i] := t;
              storeIndex := storeIndex+1;
            }
            i := i+1;
        }
        t := a[right-1];
        a[right-1] := a[storeIndex];
        a[storeIndex] := t;
        qsort(a,left,storeIndex);
        qsort(a,storeIndex+1,right);
    }  
  }
  method Testing (a: array&lt;int&gt;)
    requires  a.Length &gt; 0
    modifies a
  {
      qsort(a,0,a.Length);
      var i :int := 0;
      while(i&lt;a.Length-1)
        decreases a.Length - 1 - i
      {
        assert a[i] &lt;= a[i+1];
        i := i+1;
      }    
  }
  </code></pre>
  
  <p>But the postcondition of qsort may not hold, what can i do to correct it?</p></li>
  </ol>
  
  <p>My final verified code:</p>
  
  <pre><code>    method qsort(a: array&lt;int&gt;,left: int,right: int)
          requires 0&lt;= left &lt;= right &lt;= a.Length
          requires  0 &lt;= left &lt;= right &lt; a.Length ==&gt; forall j:: left &lt;= j &lt; right ==&gt; a[j] &lt; a[right]
          requires  0 &lt; left &lt;= right &lt;= a.Length ==&gt; forall j:: left &lt;= j &lt; right ==&gt; a[left-1] &lt;= a[j]
          ensures forall j,k:: left &lt;= j &lt; k &lt; right ==&gt; a[j] &lt;= a[k]
          ensures forall j:: (0&lt;= j &lt; left) || (right &lt;= j &lt; a.Length) ==&gt; old(a[j])==a[j]
          ensures 0&lt;= left &lt;= right &lt; a.Length ==&gt; forall j:: left &lt;= j &lt; right ==&gt; a[j] &lt; a[right]
          ensures 0&lt; left &lt;= right &lt;= a.Length ==&gt; forall j:: left &lt;= j &lt; right ==&gt; a[left-1] &lt;= a[j]
          modifies a
          decreases right - left
      {
        if (right &gt; left)
        {
            var pivot := left;
            var i :int := left + 1;
            while i &lt; right
              invariant left &lt;= pivot &lt; i &lt;= right
              invariant forall j::left &lt;= j &lt; pivot ==&gt; a[j] &lt; a[pivot]
              invariant forall j::pivot &lt; j &lt; i ==&gt; a[pivot] &lt;= a[j]
              invariant forall j::0 &lt;= j &lt; left || right &lt;= j &lt; a.Length ==&gt; old(a[j])==a[j]
              invariant 0 &lt;= left &lt;= right &lt; a.Length ==&gt; forall j:: left &lt;= j &lt; right ==&gt; a[j] &lt; a[right]
              invariant 0 &lt; left &lt;= right &lt;= a.Length ==&gt; forall j:: left &lt;= j &lt; right ==&gt; a[left-1] &lt;= a[j]
              decreases right - i
            {
                if a[i] &lt; a[pivot]
                {
                  var count :=i -1;
                  var tmp:=a[i];
                  a[i] := a[count];
                  while (count&gt;pivot)
                    invariant a[pivot] &gt; tmp
                    invariant forall j::left &lt;= j &lt; pivot ==&gt; a[j]&lt;a[pivot]
                    invariant forall j::pivot&lt; j &lt; i+1 ==&gt; a[pivot]&lt;=a[j]
                    invariant forall j::0&lt;=j&lt;left || right &lt;= j &lt;a.Length ==&gt; old(a[j])==a[j]
                    invariant 0 &lt;= left &lt;= right &lt; a.Length ==&gt; forall j:: left &lt;= j &lt; right ==&gt; a[j] &lt; a[right]
                    invariant 0 &lt; left &lt;= right &lt;= a.Length ==&gt; forall j:: left &lt;= j &lt; right ==&gt; a[left-1] &lt;= a[j]
                    {
                      a[count+1]:=a[count];
                      count:=count-1;
                    }
              a[pivot+1]:=a[pivot];
              pivot:=pivot+1;
              a[pivot-1]:=tmp;
              }
                i := i+1;
            }
            qsort(a,left,pivot);
            qsort(a,pivot+1,right);
        }  
      }
      method Testing (a: array&lt;int&gt;)
        requires  a.Length &gt; 0
        modifies a
      {
          qsort(a,0,a.Length);
          var i :int := 0;
          while(i&lt;a.Length-1)
            decreases a.Length - 1 - i
          {
            assert a[i] &lt;= a[i+1];
            i := i+1;
          }
      }
  </code></pre>