Verifying Vector Addition?

Question

I'm trying to verify a vector add function in Whiley. This is what I had so far:

function add(int[] v1, int[] v2) -> (int[] v3)
requires |v1| == |v2|
ensures |v3| == |v1|:
    //
    v3 = v1
    //
    for i in 0..|v3|:
        v3[i] = v1[i] + v2[i]
    //
    return v3

However, verifying this on whileylabs produces an error saying "possible index out of bounds" on v1[i]. I'm a bit confused as this seems OK to me!

Answer 1

The issue here is that Whiley does not (at this time) automatically infer a loop invariant connecting the size of v3 and v1. Since v3 is modified in the loop, information we know about it from before the loop is lost (i.e. that |v1| == |v3|). This version verifies:

function add(int[] v1, int[] v2) -> (int[] v3)
requires |v1| == |v2|
ensures |v3| == |v1|:
    //
    v3 = v1
    //
    for i in 0..|v3| where |v1| == |v3|:
        v3[i] = v1[i] + v2[i]
    //
    return v3