#include <vcc.h>
int main()
{
int x=39;
int d=10;
int lq = 0;
int lr = x;
while (lr >= d)
_(invariant x == d*lq + lr && x %d ==lr%d )
{
if(x==39) break ;
lq=lq+1;
lr =lr d;
}
_( assert lr==39)
return 0;
}
I think I have supplied enough information with the invariant , but the assertion 'lr==39' did not verify .Why?
And where can I find the verification condition for the _(assert lr==39)?
Verification condition in my opinion is a formula like X>5 ==> X>4 ( we can infer X>4 from X>5) ,
thanks.
