title: (Dafny) Adding elements of an array into another - loop invariant
body: <p>I have a function <code>sum</code> that takes two arrays <code>a</code> and <code>b</code> as inputs and modifies <code>b</code> such that <code>b[i] = a[0] + a[1] + ... + a[i]</code>. I wrote this function and want to verify it with Dafny. However, Dafny tells me that my loop invariant might not be maintainted by the loop. Here is the code :</p>
  
  <pre><code>function sumTo(a:array&lt;int&gt;, n:int) : int
    requires a != null;
    requires 0 &lt;= n &lt; a.Length;
    decreases n;
    reads a;
  {
      if (n == 0) then a[0] else sumTo(a, n-1) + a[n]
  }
  
  method sum(a:array&lt;int&gt;, b:array&lt;int&gt;)
      requires a != null &amp;&amp; b != null
      requires a.Length &gt;= 1
      requires a.Length == b.Length
      modifies b
      ensures forall x | 0 &lt;= x &lt; b.Length :: b[x] == sumTo(a,x)
  {
      b[0] := a[0];
      var i := 1;
  
      while i &lt; b.Length
          invariant b[0] == sumTo(a,0)
          invariant 1 &lt;= i &lt;= b.Length
  
          //ERROR : invariant might not be maintained by the loop.
          invariant forall x | 1 &lt;= x &lt; i :: b[x] == sumTo(a,x)
  
          decreases b.Length - i
      {
          b[i] := a[i] + b[i-1];
          i := i + 1;
      }
  }
  </code></pre>
  
  <p>How can I fix this error?</p>