original.name="DoWhile_Valid_1"
======
>>> main.whiley


method f(int[] args) -> int
requires |args| >= 2:
    //
    int r = 0
    int i = 0
    do:
        r = r + args[i]
        i = i + 1
    while (i + 1) < |args| where i >= 0
    //
    return r

public export method test():
    int result = f([1, 2, 3])
    assume result == 3
    //
    result = f([1, 2])
    assume result == 1
    //
    result = f([1, 2, 3, 4, 5, 6])
    assume result == 15

---