Verification issue

[TonyP4N]

Failing code

function integer_squareroot(n: int): (x: int)
    ensures res * res <= n
{
    var x := 0;
    var y := (x + 1) / 2;
    while y < x
        invariant y * y <= n
        invariant x * x <= n
        invariant y >= 0
    {
        x := y;
        y := (x + n / x) / 2;
    }
    return x;
}

Steps to reproduce the issue

• Dafny version: 4.3.0.0
• Dafny VSCode extension version: 3.2.1

Actual behavior

always report invalid UnaryExpressionParser[p_generic_syntax_error] on the while key word

[keyboardDrummer]

To use a while loop, you need to use a method, like so:

method integer_squareroot(n: int) returns (res: int)
    ensures res * res <= n
{
    var x := 0;
    var y := (x + 1) / 2;
    while(y < x)
        invariant y * y <= n
        invariant x * x <= n
        invariant y >= 0
    {
        x := y;
        y := (x + n / x) / 2;
    }
    return x;
}

But I admit that the difference between allowed bodies for methods (allows statements) and functions (only allows an expression) can be surprising.

[TonyP4N]

That makes sense, thank you very much!