Is this a bug?

[vkensou]

function sum(int[] items) -> int
requires all{ q in 0..|items| | items[q] >= 0}:
    int i = 0
    int r = 0
    while i < |items| where r >= 0:
        r = r + items[i]
\\                    ~  
        i = i + 1
    return r

Type these code in http://whileylabs.com/. Then select "Verification". It said: "Possible index out of bounds(negative)" in the line:"r = r + items[i]". What's wrong with me?

[vkensou]

sorry. I haven't finished reading the document. Please delete this discussion.

[vkensou]

The following code is correct:

function indexOf(int[] items, int item) -> (int|null r)
ensures r is int ==> items[r] == item
ensures r is null ==> all { j in 0..|items| | items[j] != item }
ensures r is int ==> all { j in 0 .. r | items[j] != item }:
    int i = 0
    while i < |items| where i >= 0:
\\                          ~~~~~~
        if items[i] == item:
            return i
        i = i + 1
    return null

[DavePearce]

Hey, all good. Sorry I've only just noticed the discussions!! I'd suggest raising issues will get my attention more quickly. It doesn't matter what kinds of questions you ask --- I'm happy to answer them all!