title: Dafny: copy array region method validation
body: <p>I am working on a language comparison of several languages created with verification in mind (Whiley, Dafny and Frama-C etc.) I was given this example of a function which copied a region of one array to another array with different placement within the destination array. The specification I came up with looks like this in Dafny:</p>
  
  <pre><code>method copy( src: array&lt;int&gt;, sStart: nat, dest: array&lt;int&gt;, dStart: nat, len: nat)
      returns (r: array&lt;int&gt;)
    // both arrays cannot be null
     requires dest != null &amp;&amp; src != null
    // Source array must contain enough elements to be copied
     requires src.Length &gt;= sStart + len
    // Destination array must have enough space for copied elements
     requires dest.Length &gt;= dStart + len
    // Result is same size as dest
    ensures r != null
    ensures r.Length == dest.Length
    // All elements before copied region are same
     ensures r[..dStart] == dest[..dStart]
    // All elements above copied region are same
     ensures r[dStart + len..] == dest[dStart + len..]
    // All elements in copied region match src
     ensures forall k: nat :: k &lt; len ==&gt; r[dStart + k] == src[sStart + k]
  
  {
      if len == 0 { return dest; }
      assert len &gt; 0;
      var i: nat := 0;
      r := new int[dest.Length];
      while (i &lt; r.Length)
        invariant i &lt;= r.Length
        decreases r.Length - i
        invariant r.Length == dest.Length
        invariant forall k: nat :: k &lt; i ==&gt; r[k] == dest[k]
      {
          r[i] := dest[i];
          i := i + 1;
      }
      assume r[..] == dest[..];
      i := 0;
      while (i &lt; len)
        invariant i &lt;= len
        decreases len - i
        invariant r.Length == dest.Length
        invariant r.Length &gt;= dStart + i
        invariant src.Length &gt;= sStart + i
        invariant r[..dStart] == dest[..dStart]
        invariant r[(dStart + len)..] == dest[(dStart + len)..]
        invariant forall k: nat :: k &lt; i ==&gt; r[dStart + k] == src[sStart + k]
      {
          r[dStart + i] := src[sStart + i];
          i := i + 1;
      }
  }
  </code></pre>
  
  <p>In the second while loop above there may be some unneeded invariants as I have tried to cover everything I can think of. but, yeah, this doesn't verify and I am perplexed as to why...</p>
  
  <pre><code>Dafny/copy.dfy(35,4): Error BP5003: A postcondition might not hold on this return path.
  Dafny/copy.dfy(17,11): Related location: This is the postcondition that might not hold.
  Execution trace:
      (0,0): anon0
      (0,0): anon19_Else
      Dafny/copy.dfy(24,5): anon20_LoopHead
      (0,0): anon20_LoopBody
      Dafny/copy.dfy(24,5): anon21_Else
      (0,0): anon23_Then
      Dafny/copy.dfy(35,5): anon24_LoopHead
      (0,0): anon24_LoopBody
      Dafny/copy.dfy(35,5): anon25_Else
      (0,0): anon27_Then
  Dafny/copy.dfy(43,16): Error BP5005: This loop invariant might not be maintained by the loop.
  Execution trace:
      (0,0): anon0
      (0,0): anon19_Else
      Dafny/copy.dfy(24,5): anon20_LoopHead
      (0,0): anon20_LoopBody
      Dafny/copy.dfy(24,5): anon21_Else
      (0,0): anon23_Then
      Dafny/copy.dfy(35,5): anon24_LoopHead
      (0,0): anon24_LoopBody
      Dafny/copy.dfy(35,5): anon25_Else
      Dafny/copy.dfy(35,5): anon27_Else
  
  Dafny program verifier finished with 1 verified, 2 errors
  </code></pre>