janhaag/PSE2011 — Issue #96: Incompleteness in proving recursive methods
Author: danielbruns
Created: 2012-03-05 12:26:58+00:00
State: open

Try this program:
int foo (int x)
assume x >= 0;
{
int y;
if (x > 0) { y = 1+foo(x-1); }
return y;
}
ensure x == y;

main (int z)
{
z = foo(z*z);
}

The verifier will say "FunctionEnsureToRemainingProgram, Line 5 false; y$1$0 = 0 x$0 = 2 x$1$0 = 0".
Apart from the cryptic syntax, I don't understand why the postcondition cannot be proven.