how come this function verified?

Apr 22, 2011 at 2:03 PM

int metricf(int x)
 requires(0 < x && x < 20)
 ensures(x<20)
{
    x=x+1;
    return x;
}

i am new to this vcc  ,what if x takes a value 19 ?, otherwise it choose value of x while taking care of x=x+1 ? 

Apr 22, 2011 at 2:26 PM

You need to use the result keyword to write postconditions concerning the result of the function:

int metricf(int x)
 requires(0 < x && x < 20)
 ensures(result <= 20)
{
    x = x + 1;
    return x;
}

Daniel

Apr 22, 2011 at 2:29 PM

thanks mate

sorry i was dumb i thought i used result there:|