title: Verifying a Dafny method that shifts a region of an array
body: <p>I'm using Dafny to make a delete method where you receive: </p>
  
  <ul>
  <li><p>char array <code>line</code> </p></li>
  <li><p>the length of the array <code>l</code></p></li>
  <li><p>a position <code>at</code></p></li>
  <li><p>the number of characters to delete <code>p</code></p></li>
  </ul>
  
  <p>First you delete the characters of line from at to <code>at + p</code>, and then you must move all the characters on the right of <code>at + p</code> to <code>at</code>.</p>
  
  <p>For example, if you have <code>[e][s][p][e][r][m][a]</code>, and <code>at = 3</code>, and <code>p = 3</code>, then the final result should be <code>[e][s][p][a]</code></p>
  
  <p>I'm trying to prove a postcondition that makes sense like:</p>
  
  <p><code>ensures forall j :: (at&lt;=j&lt;l) ==&gt; line[j] == old(line[j+p]);</code> </p>
  
  <p>To ensure that all chars from the right of at + p are in the new positions.</p>
  
  <p>But Dafny outputs two errors:</p>
  
  <blockquote>
    <p>index out of range  7   53</p>
    
    <p>postcondition might not hold on this return path.   19  2</p>
  </blockquote>
  
  <pre><code>method delete(line:array&lt;char&gt;, l:int, at:int, p:int)
    requires line!=null;
    requires 0 &lt;= l &lt;= line.Length &amp;&amp; p &gt;= 0 &amp;&amp; at &gt;= 0;
    requires 0 &lt;= at+p &lt;= l;
    modifies line;
    ensures forall j :: (at&lt;=j&lt;l) ==&gt; line[j] == old(line[j+p]) ; 
  {
    var tempAt:int := at;
    var tempAt2:int := at;
    var tempPos:int := at+p;
    while(tempAt &lt; at + p)
      invariant at&lt;=tempAt&lt;=at + p;
    { 
      line[tempAt] := ' ';
      tempAt := tempAt + 1;
    }
  
    while(tempPos &lt; line.Length &amp;&amp; tempAt2 &lt; at + p)
      invariant at + p&lt;=tempPos&lt;=line.Length;
      invariant at&lt;=tempAt2&lt;=at+p;
    {
      line[tempAt2] := line[tempPos];
      tempAt2 := tempAt2 + 1; 
      line[tempPos] := ' ';
      tempPos := tempPos + 1;
    }
  }
  </code></pre>
  
  <p><a href="http://rise4fun.com/Dafny/xqqL" rel="nofollow">Here is the program on rise4fun</a></p>