original.name="While_Valid_70"
======
>>> main.whiley
function sq(int n) -> (int r) requires n >= 0
ensures r == n * n:
    int i = 0
    int prod = 0
    //
    while i < n
    where i >= 0 && prod == i * n
    where i <= n:
        i = i + 1
        prod = prod + n
    //
    return prod

public export method test():
    assert sq(0) == 0
    assert sq(1) == 1
    assert sq(2) == 4
    assert sq(3) == 9
---