
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?



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);

