title: dafny implementation of insertionsort
body: <p>i am new in Dafny and i have problems verifying my insertionSort-implementation.
  Dafny tells me the the multiset invariants are not holding, anything else is working fine. After Hours of searching the mistake i could need some help :)
  Would be nice if somebody could tell me the trick!</p>
  
  <p>My Code:</p>
  
  <pre><code>predicate sorted(a:array&lt;int&gt;, min:int, max:int)
  requires a != null;
  requires 0&lt;= min &lt;= max &lt;= a.Length;
  reads a;
  {
    forall j, k :: min &lt;= j &lt; k &lt; max ==&gt; a[j] &lt;= a[k]
  }
  
  
  /*
   *  
   */  
  method insertionSort(a: array&lt;int&gt;)
  requires a != null;
  requires a.Length &gt; 0;
  ensures sorted(a, 0, a.Length);
  ensures multiset(a[..]) == multiset(old(a[..]));
  modifies a; 
  {
    var i := 1; 
  
    while(i &lt; a.Length)
    invariant 1 &lt;= i &lt;= a.Length;
    invariant sorted(a, 0, i); 
    invariant a != null;
    invariant multiset(old(a[..])) == multiset(a[..]);
    decreases a.Length-i;
    {
      var j := i - 1;
      var key := a[i];
  
     while(j &gt;= 0 &amp;&amp; key &lt; a[j])
     invariant -1 &lt;= j &lt;= i - 1 &lt;= a.Length;
     invariant (j == i-1 &amp;&amp; sorted(a, 0, i)) || (sorted(a, 0, i+1));
     invariant forall k :: j &lt; k &lt; i ==&gt; a[k] &gt;= key; 
     invariant -1 &lt; j == i - 1   ==&gt; multiset(old(a[..])) == multiset(a[..]);
     invariant |multiset(old(a[..]))| == |multiset(a[..])|;
     invariant -1 &lt; j &lt; i - 1 &amp;&amp; key &lt; a[j] ==&gt; multiset(old(a[..]))  ==  multiset(a[..]) - multiset({a[j+1]}) + multiset({key});
     invariant -1 == j ==&gt; multiset(old(a[..]))  ==  multiset(a[..]) + multiset({key}) - multiset({a[j+1]});
     decreases j;                                         
     {
  
       a[j + 1] := a[j];
  
       j := j - 1;
  
     }
  
     a[j + 1] := key;
     i := i + 1; 
     }
  } 
  </code></pre>
  
  <p>It produces</p>
  
  <pre><code>1   This loop invariant might not be maintained by the loop.    29,38
  2   This loop invariant might not be maintained by the loop.    42,73
  3   This loop invariant might not be maintained by the loop.    43,52
  </code></pre>
  
  <p>Link: <a href="http://rise4fun.com/Dafny/3R5" rel="nofollow">http://rise4fun.com/Dafny/3R5</a></p>