Why does function need (impractical) coaching?

Apr 30, 2014 at 4:19 PM
What am I missing?

// Sum of elements between indices b(egin and e(nd
function method sum(a: array<int>, b: int, e: int): int
requires a != null;
requires 0 <= b <= e < a.Length; // b and e are indices in a
reads a;
decreases e - b;
{
if (b == e) then a[b] // length 1
else sum(a, b, e - 1) + a[e] // a[0] + sum(b + 1, e) preferable but failed Test()
}

method Test()
{
var a: array<int> := new int[4];
a[0], a[1], a[2], a[3] := -9, 6, 7, 8;
assert sum(a, 1, 2) == 13;
assert sum(a, 1, 3) == 21;
}

method Test1()
{
var a: array<int> := new int[4];
a[0], a[1], a[2], a[3] := -9, 6, 7, 8;
//assertion violation(?!) assert sum(a, 1, 3) == 21;
}
Apr 30, 2014 at 11:02 PM
I suppose I am to use sequences here rather than arrays, because following is OK (supported in documentation?):

// Sum of elements between indices b(egin and e(nd
function sum(a: seq<int>, b: int, e: int): int
requires 0 <= b <= e < |a|; // b and e are indices in a
decreases e - b;
{
if (b == e) then a[b] // length 1
else sum(a, b, e - 1) + a[e] // a[0] + sum(b + 1, e) preferable but failed Test()
}

method Test()
{
var a: seq<int> := [-9, 6, 7, 8];
assert sum(a, 1, 2) == 13;
assert sum(a, 1, 3) == 21;
}

method Test1()
{
var a: seq<int> := [-9, 6, 7, 8];
assert sum(a, 1, 3) == 21;
}
May 2, 2014 at 8:11 PM
I don't know for sure, but it appears that there is some issue with verification of functions when the termination measure is hit. Here is another version of your code that exhibits the same type, but mirrored problem:

// Sum of elements between indices b(egin and e(nd
function method sum(a: array<int>, b: int, e: int): int
requires a != null;
requires 0 <= b <= e < a.Length; // b and e are indices in a
reads a;
decreases e - b;
{
if (b == e) then a[b] // length 1
else a[b] + sum(a, b + 1, e)
}

method Test()
{
var a: array<int> := new int[4];
a[0], a[1], a[2], a[3] := -9, 6, 7, 8;
assert sum(a, 2, 3) == 15;
assert sum(a, 1, 3) == 21;
}

method Test1()
{
var a: array<int> := new int[4];
a[0], a[1], a[2], a[3] := -9, 6, 7, 8;
assert sum(a, 1, 3) == 21;
}