
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 ?



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



thanks mate
sorry i was dumb i thought i used result there:

