title: Dafny-recursiveSum assertion violation
body: <p>I tried to write a recursive sum function in dafny and prove its correctness. I have written:</p>
  
  <pre><code>method Main() {
  var a: array&lt;int&gt; := new int[4];
  a[0] := 7;
  a[1] := -2;
  a[2] := 3;
  a[3] := -2;
  assert a[..] == [7,-2,3,-2];
  
  var s/*, p, c */:= Sum(a, -2);
  assert a[0] == 7 &amp;&amp; a[1] == -2 &amp;&amp; a[2] == 3 &amp;&amp; a[3] == -2;
  assert s == RecursiveSum(a, 0); // == 6
  print "\nThe sum of all elements in [7,-2,3,-2] is ";
  print s;
  }
  
  function RecursiveSum(a: array&lt;int&gt;, from: nat) : int
  reads a
  requires a != null
  requires from &lt;= a.Length
  decreases a.Length-from
  {
  if from == a.Length then 0
  else a[from] + RecursiveSum(a, from+1)
  }
  </code></pre>
  
  <p>This is the prove I wrote :</p>
  
  <pre><code>method Sum(a: array&lt;int&gt;, key: int) returns (s: int)
  requires a != null
  ensures s == RecursiveSum(a, 0)
  
  {   
  // Introduce local variable (6.1)
  var i : nat; //frame s ,i
  s,i:=sum1(a);
  // Strengthen post condition (1.1)
  assert i== a.Length &amp;&amp; s == RecursiveSum(a,0);
  
  }
  </code></pre>
  
  <p>SUM1:</p>
  
  <pre><code>method sum1(a: array&lt;int&gt;) returns (s : int, i : nat)
  requires a != null
  ensures  i== a.Length &amp;&amp; s == RecursiveSum(a,0);
  {
  assert  RecursiveSum(a,a.Length)==0 ;
  //  Assignment (1.3)
  s,i:=0,0;
  assert  0 &lt;= i &lt;= a.Length &amp;&amp; s==RecursiveSum(a,i) ;
  
  // Iteration (5.5)
  while (i != a.Length)
    invariant  0 &lt;= i &lt;= a.Length &amp;&amp; s==RecursiveSum(a,i) ;
  decreases  a.Length-i ;
  {
  assert 0 &lt;= i &lt;=a.Length &amp;&amp; RecursiveSum(a,i)==s &amp;&amp; i!=a.Length  ;
      s, i := Sum2(s, a, i);
  }
  assert i== a.Length &amp;&amp; s == RecursiveSum(a,0);
  }
  </code></pre>
  
  <p>SUM2:</p>
  
  <pre><code>method Sum2(s0 : int, a: array&lt;int&gt;, i0 : nat) returns (s : int, i : nat)
  requires a != null
  requires 0 &lt;= i0 &lt;= a.Length &amp;&amp; RecursiveSum(a,i0)==s0 &amp;&amp; i0 != a.Length;
  ensures RecursiveSum(a,0)==s &amp;&amp; 0 &lt;= i &lt;= a.Length;
  {
  // Assignment (1.3)
  s, i := s0, i0;
  // Contract frame (5.4)
  assert 0 &lt;= i0 &lt;= a.Length &amp;&amp; RecursiveSum(a,i0)==s0 &amp;&amp; RecursiveSum(a,i0+1)==s0+a[i] ;
  // leading assignment (8.5)
  s := s0 + a[i];
  assert 0 &lt;= i0 &lt;= a.Length &amp;&amp; RecursiveSum(a,i0)==s0 &amp;&amp; RecursiveSum(a,i0+1)==s0+a[i] ;
  i := i + 1;
  assert  0 &lt;= i &lt;=a.Length &amp;&amp; RecursiveSum(a,0)==s &amp;&amp; 0 &lt;= a.Length-i &lt; a.Length-i0 ;
  }
  </code></pre>
  
  <p>The errors I get :</p>
  
  <pre><code>stdin.dfy(75,32): Error: assertion violation 
  stdin.dfy(78,1): Error: decreases expression might not decrease
  stdin.dfy(79,37): Error BP5005: This loop invariant might not be maintained   by the loop.
  stdin.dfy(96,77): Error: assertion violation
   stdin.dfy(101,47): Error: assertion violation
  </code></pre>
  
  <p>Please help me understand why ?</p>