I'm a bit boggled by this question, when I ran this program I got results greater than 0 but I'm not sure if that would always be the case since the program could execute x++ or x-- first in theory. How can I definitively confirm that the results will always be bigger than 0 ?
proctype testcount(byte x)
{
do
:: (x != 0 ) ->
if
:: x ++
:: x --
:: break
fi
:: else -> break
od;
printf("counter = %d\n", x);
}
init {run testcount(1)}
This can be easily verified by extending the model with the property you want to verify:
Complete Model:
Generate a verifier, and run it:
As witnessed by the result of the above verification, property
larger_or_equal
is always true whereas propertystrictly_larger
can be false.