possible bug?

Apr 15, 2016 at 2:09 AM
For this code:
function method sum (s: seq<int>) : int
{
  if |s| == 0 then 0 
  else s[0] + sum(s[1..])   
}

class KV 
{
  var key : int;
  var value : int;
  
  predicate equals (o: KV) 
  reads this, o
  requires o != null
  {
    this.key == o.key && this.value == o.value
  }
}

predicate seqEquals (l1: seq<KV>, l2: seq<KV>)
reads l1, l2
{
  (|l1| == |l2| && 
   forall i: int :: 0 <= i < |l1| ==>
     (l1[i] == null && l2[i] == null) || 
     (l1[i] != null && l2[i] != null && l1[i].equals(l2[i]))
  ) 
}


predicate isMRList (l1: seq<int>, l2: seq<KV>)
reads l2
{
  |l1| == |l2| && 
  forall i: int :: 0 <= i < |l2| ==> l2[i] != null && l2[i].value == l1[i]
}

method mapper (input: seq<int>) returns (output: seq<KV>) 
ensures isMRList(input, output)
{  
  if |input| == 0 
  { output := []; }
  else
  {
    var v := new KV;
    v.key := 0;
    v.value := input[0];
  
    var l := mapper(input[1..]);
    output := [v] + l; 
  } 
} 


method reduce (input: seq<KV>) returns (l: seq<int>, output: int)
requires forall i: int :: 0 <= i < |input| ==> input[i] != null
ensures isMRList(l, input) && sum(l) == output 
{
  if |input| == 0
  { output := 0; 
    l := [];
  }
  else
  {
    var s1,s2 := reduce(input[1..]);
    output := input[0].value + s2;
    l := [input[0].value] + s1;
  } 
}


method test (input: seq<int>)
{
  var v1 := mapper(input);
  var v2,v3 := reduce(v1);

  assert input == v2;
  assert v3 == sum(input);
}
I got assertion violation if I switch the order of
  assert input == v2;
  assert v3 == sum(input);
in test. Is there a reason why that is the case?
Apr 15, 2016 at 12:43 PM
I think input == v2 is an intermediate assertion to infer v3 == sum(input).

the postconditions fromvar v1 := mapper(input); var v2,v3 := reduce(v1); are:
v1 is a sequence of KV which is generated based on the sequence input by fill the filed key with 0
v2 is a sequence of int which projects the filed value from v1
sum (v2) == v3


It is not surporised that dafny needs you to provide a hints that input == v2 in order to prove v3 == sum(input);