May 13, 2011 at 4:22 AM
Edited May 13, 2011 at 4:24 AM

Hi there,
I am working on the exercises in the tutorial document (4/18/2011 version) and got stuck at an assertion that says int x is a perfect square. I wrote
int x;
_(assert \exists int i; 0 <= i && i <= x && x == i*i),
But the verification failed. I can't see anything wrong in my assertion. Any help? Thanks.
JH


Editor
May 13, 2011 at 9:07 AM

If this is your entire program, then the assertion does not generally hold: not all integers are perfect squares.
In general, to be able to prove an existential assertion in program verification, one explicitly shows a witness (an instance of the quantified variable such that the formula holds).
In the case of the perfect square example, one simple way of doing so would be to show that x is a perfect square
by construction. For example, in the following program (disregarding arithmetic overflows at the moment, but VCC will require you to pay attention to them), x is a perfect square, and VCC should be able to prove it (there may be other issues, such
as triggers and similar problems that are discussed further down the line in the tutorial).
int y;
int x = y * y;
_(assert \exists int i; i <= x && x == i * i ) // VCC should be able to prove that y <= x and x == y * y, and therefore prove the existential generalisation
Also, notice I dropped the 0 <= i constraint, which is actually not useful for that particular exercise. As for the exercise itself, I think (but Michal could provide confirmation if he drops by) that the idea is mostly to simply write the assertion, to
familiarise yourself with the annotation language, without trying to run it through VCC. You did a good job out of that.
I hope this helped,
Francois



Thanks for the help. Your assertion works better than mine. VCC doesn't have any complain other than the overflow.
But I was able to confuse VCC by a minor change as follows.
#include <vcc.h>
int main()
{
int x;
x = 4; // x = 4*4;
_(assert \exists int i; i <= x && x == i*i)
return 0;
}
The verification again fails. Does it mean I can't use constant in assertion? Thanks.
JH


Editor
May 13, 2011 at 4:13 PM

You can definitely use constants in assertions. I think the problem here is that VCC simply has trouble proving the assertion without hints.
I suggest you keep reading through the tutorial and see if you can come back to this problem at the end and figure out how to make it work. One easy way is as follows:
#include <vcc.h>
int main()
{
int x;
_(ghost int y;)
_(ghost y = 2;)
x = 4;
_(assert x == y * y)
_(assert \exists int i; i <= x && x == i * i)
return 0;
}
But my challenge to you is to do the same thing without the ghost variable or the intermediate assertion. Hint: I have no idea how to do it, but I'm sure it will involve triggers :)



Thanks for the input. It makes sense to put aside those details till read through the tutorial back and forth a few times. I'll come back to those assertions ;0) Have a good one.

