======
>>> main.whiley
function f(int x, int y) -> (int r)
requires x <= y
ensures r >= 0:
    r = 0
    //
    for i in x..y
    where r >= 0:
        x = 0
        r = r + 1
    //
    return r

public export method test():
    assume f(0,0) == 0
    assume f(-1,0) == 1
    assume f(-1,3) == 4    
---