
To be a little more clear than the brief title. I would like to prove that foreach 1 < i < MAX_PRIME: prime[i] <==> is_prime(i). Or, prime[p] contains the boolean integer of whether p is prime.
Everything seems to be fine except for the last assertion. But then the second ensures for isPrime starts giving an error.
#include <vcc.h>
#include <stdio.h>
#include <stdlib.h>
#include <math.h>
#define MAX_PRIME 100
char prime[MAX_PRIME+1];
char isPrime(int n)
_(requires n > 1)
_(requires n <= MAX_PRIME)
_(ensures \exists int i; i > 1 && i < n ==> (n% i == 0 ==> \result == 0))
_(ensures \forall int i; i > 1 && i < n ==> (n%i != 0 ==> \result == 1))
_(ensures \result == 0  \result == 1)
{
int i=2;
_(assert n*n < INT_MAX)
while(1)
{
if(n%i == 0)
return 0;
++i;
}
//for(i=2;i*i < n ; ++i)
//{
// if(n%i == 0)
// return 0;
//}
return 1;
}
int main()
_(requires \thread_local_array(prime, MAX_PRIME+1))
_(writes \array_range(prime, MAX_PRIME+1))
// _(ensures \forall int p; p > 1 && p <= MAX_PRIME ==> (prime[p] <==> \forall int i; i > 1 && i < p ==> p% i != 0))
{
int i;
prime[0] = 0;
prime[1] = 0;
for(i=2; i <= MAX_PRIME; ++i)
{
prime[i] = isPrime(i);
//if(prime[i])
// printf("%d\n", i);
}
//check that each entry in prime is true iff the corrensponding index is prime
_(assert \forall int p; p > 1 && p <= MAX_PRIME ==> (prime[p] <==> \forall int i; i > 1 && i < p ==> p% i != 0))
//system("PAUSE");
return 0;
}
I'm having trouble understanding the output of Z3. According to the manual, you're supposed to be able to see what kind of progress it made with the proof, but I can't tell what the problem is.



Hi,
There are several things that go wrong here.
First, your postconditions for isPrime, although (I believe) correct, are kind of convoluted. I would write something along the lines of "the result is a boolean that encodes whether n is prime". In VCC, I would write this:
_(ensures \result <==> (\forall int i; 1 < i ==> i < n ==> n % i != 0))
You can keep the last postcondition, which is not actually necessary in your development, but doesn't harm it either...
Then, you are missing loop invariants. In your case (in the loop that you commented out, not the nonterminating aberration that's currently in there), they are simple: you know that for any j less than the loop index, j does not divide n. (_(invariant
\forall int j; 1 < j ==> j < i ==> n % j != 0), for example). You may need another invariant stating that i remains less than n, and you need to fix your loop so that it performs the division by 2 instead of skipping it, but other than that, VCC
should like it.
What it won't like, however, is the extra bit of reasoning that's required to prove that, if n has no nonunit divisors less than or equal to sqrt(n), then it has no divisors other than 1 and itself. Currently, and until someone smarter than me chimes in
with a way of making VCC prove this, I would suggest you simply change your loop condition to "i < n" instead of "i * i < n" (which is incorrect, by the way, you *definitely* need to check if i divides n when i * i = n...).
With those simple changes, and similar changes in main() (which I will let fix), everything should go through. Again, don't forget to iterate over 2 as well...
Hope this helps,
Francois



Ok, I performed some of the cleanup you suggested. VCC still doesn't accept the final proof. Only the final assert shows a blue wavy line, but in z3 I'm seeing other errors, so I'm confused as to what's going on.
I added an assertion which actually says that the primality of i is being stored in prime[i] the main loop, but that doesn't fix the proof. I also added invariants which say that i can't overflow, but it still seems to think it can in
the main loop. Apparently you can't copy text out of Z3, but this is what I'm seeing:
https://skydrive.live.com/redir?resid=BCA8FC90DF320175!108&authkey=!AAst2arwWh2PxAM
I don't understand why I'm getting the errors for lines 33,34, and 36.
#include <vcc.h>
#include <stdio.h>
#include <stdlib.h>
#include <math.h>
#define MAX_PRIME 100
char prime[MAX_PRIME+1];
char isPrime(int n)
_(requires n > 1)
_(requires n <= MAX_PRIME)
_(ensures \result <==> (\forall int i; i > 1 && i < n ==> n % i != 0))
{
int i=2;
for(i=2;i < n ; ++i)
_(invariant \forall int j; j > 1 && j < i ==> n % j != 0)
_(invariant i + 1 < INT_MAX)
{
if(n%i == 0)
return 0;
}
return 1;
}
int main()
_(requires \thread_local_array(prime, MAX_PRIME+1))
_(writes \array_range(prime, MAX_PRIME+1))
{
int i;
for(i=2; i <= MAX_PRIME; ++i)
_(invariant i + 1 < INT_MAX)
{
prime[i] = isPrime(i);
//if(prime[i])
// printf("%d\n", i);
_(assert prime[i] <==> (\forall int j; j > 1 && j < i ==> i % j != 0))
}
//check that each entry in prime is true iff the corrensponding index is prime
_(assert \forall int p; p > 1 && p <= MAX_PRIME ==> (prime[p] <==> \forall int i; i > 1 && i < p ==> p% i != 0))
//system("PAUSE");
return 0;
}


Oct 18, 2012 at 7:51 AM
Edited Oct 18, 2012 at 7:53 AM

The Z3 inspector you are referring to does not display actual errors, it displays potential errors. To get accurate error reports, you need to go into Visual Studio's "Output" panel, and select "Verification". The fact that the blue squiggles
only appear on the final assertion means that VCC reaches it without encountering any other errors.
Now, the problem with loops is that they need to be approximated: you can't simply unroll them in the proof and hope for the best, since you don't know how many times you'd need to unroll them. The approximation is done using invariants, and anything that
is inside the loop is hidden from the outside of the loop.
If you turn your assertion into an invariant (for example, "invariant \forall int j; 1 < j ==> j < i ==> (prime[j] <==> \forall int k; 1 < k && k < j ==> j % k != 0)"), VCC stops complaining and gives you this
"Verification of main succeeded." we all strive for. Note that all this invariant is doing is letting VCC know that the assertion you wrote is true for all indices that have already been traversed by the program. VCC also knows that, when the loop
exits, all indices up to MAX_PRIME have been traversed and can then conclude with your final assertion.
The basic lesson is: when working with loops, you need to abstract them into invariants for VCC before you can prove anything about them.
Also, don't worry about the Z3 inspector until you have proofs that take longer than 30 seconds to go through: it is only useful on very long proofs to see where VCC is getting lost and figure out how you can guide it better.
Regards,
Francois


Oct 19, 2012 at 10:18 AM
Edited Oct 19, 2012 at 10:18 AM

As a followup, I 'd like to give a hint as to how one could possibly go about proving that your original version of isPrime, that stops when i becomes greater than the square root of n, is also correct. I have to go ahead and give you a full disclaimer:
I am not on my VCC (understand Windows) machine, and Rise4Fun appears to be down, so I have no way of testing whatever I am saying, so please take it all with a grain of salt and don't hate me too much if it doesn't work.
My original idea was to try and teach VCC enough number theory to figure out that it was enough to only check for divisors smaller than square root of n. This fails nastily, with Z3 either looping or failing almost immediately. The second solution, which
i will describe more below, is to do a proof by programming.
Basically, the idea is to have your physical loop stop at square root of n, and then use a ghost loop to iterate over the other values of i, showing, for each of them, that if i divided n, then there would have been a j smaller than square root of n that
divides n in the physical loop (namely, j = n / i). With a carefully chosen loop invariant for the ghost loop, you may be able to push the proof through, whilst retaining the slight performance improvement you get from not testing every single integer in [0..n].
The caveat is that, at the moment, i don't think this approach is entirely sound: unless you ask VCC to prove termination of isPrime, it will not check, whatever annotations you add, termination of the ghost loop, and you will have to make a side argument
for it.
I hope this helps more,
Francois



I could be curious to know how VCC works in this regard. Here is a proof for it:
http://www.math.uconn.edu/~stein/math103/Slides/math10308.pdf
It is a proof by contradiction. Also, what do you have to do to give VCC a general proof, as opposed to telling it something about the program? I tried translating the given proof to an assert statement near the beginning of the program, but it said the
assert keyword was invalid.
I did some cleanup based on the previous suggestions and got a working version. I used a macro to avoid repeating the definition of a prime number. Thought functions would be safer with regards to variable collision (which I got the first time).
Is there such a thing in VCC?
#include
#include
#include
#include
#define MAX_PRIME 100
//n is not divisible by any number less than max. max==n for the standard
//definition of a prime number
#define vccPrime(n, max) (\forall int qq; qq > 1 && qq < max ==> n % qq != 0)
char prime[MAX_PRIME+1];
char isPrime(int n)
_(requires n > 1)
_(requires n <= MAX_PRIME)
_(ensures \result <==> vccPrime(n, n))
{
int i=2;
for(i=2;i < n ; ++i)
_(invariant vccPrime(n, i))
_(invariant i + 1 < INT_MAX)
{
if(n%i == 0)
return 0;
}
return 1;
}
int main()
_(requires \thread_local_array(prime, MAX_PRIME+1))
_(writes \array_range(prime, MAX_PRIME+1))
{
int i;
for(i=2; i <= MAX_PRIME; ++i)
_(invariant i + 1 < INT_MAX)
_(invariant \forall int j; j > 1 && j < i ==> (prime[j] <==> vccPrime(j,j)))
{
prime[i] = isPrime(i);
//if(prime[i])
// printf("%d\n", i);
}
//check that each entry in prime is true iff the corrensponding index is prime
_(assert \forall int p; p > 1 && p <= MAX_PRIME ==> (prime[p] <==> vccPrime(p,p)))
//system("PAUSE");
return 0;
}



VCC provides several ways of defining macrolike things without falling prey to name capture.
The simplest one (to me) would be to use a specification function. In this case, we'll make it a def function because there is no reason to require any abstraction, and we can write:
_(def \bool vccPrime(int n,int max)
{
return \forall qq; 1 < qq ==> qq < max ==> n % qq != 0;
})
To let VCC know about the theorem you want to use, you could import it as an axiom. However, in my experience, an axiom on nonlinear arithmetic such as the one you plan on importing is not going to help you, and is probably going to cause Z3 to fail, or
even to loop indefinitely. This is something you do not want. Since Rise4Fun is now back online, I was able to check that the proof by programming does work. If you look at tit carefully, it is in fact also a proof by contradiction, very similar to the one
you refer to. After iterating over all i's less than or equal to square root of n physically, I prove for each j greater than or equal to the final i, that it is impossible for j to divide n (the _(assert \false) in the second loop). [I reexpanded the vccPrime
macro for various reasons, but it can be folded back out of sight.] The Rise4Fun version of VCC may be a bit outdated, and what verified then may no longer verify, so you might have to fiddle with the code a bit, but the idea remains the same.
char isPrime(int n)
_(requires n > 1)
_(requires n <= MAX_PRIME)
_(ensures \result <==> \forall int i; 1 < i ==> i < n ==> n % i != 0)
{
int i=2;
for(i=2; i * i <= n ; ++i)
_(invariant \forall int j; 1 < j ==> j < i ==> n % j != 0)
_(invariant 0 < i && i <= n)
{
if(n%i == 0)
return 0;
}
_(assert \forall int k; 1 < k ==> k < i ==> n % k != 0)
_(ghost {
int j = i;
for (j = i; j < n; ++j)
_(invariant \forall int k; 1 < k ==> k < j ==> n % k != 0)
_(invariant i <= j && j <= n)
{
if (n%j == 0)
{
int i0 = n / j;
_(assert n == j * i0)
_(assert i0 < i)
_(assert n % i0 == 0)
_(assert \forall int k; 1 < k ==> k < i ==> n % k != 0)
_(assert n % i0 != 0)
_(assert \false)
}
}})
return 1;
}
I would be very interested to know if you manage to make a proof that does not involve writing a ghost loop, and in particular if you manage to use nonlinear arithmetic results to make the proof, but if I were you, I wouldn't waste too much time after the
first couple of Z3 timeouts. This is just not something automated tools are good at...
In passing, note that the ghost loop is never executed and only exists when running VCC to help it with the proof. In particular, it does not change the running time or overall behaviour of the function. You can find a lot more about this in the tutorial
or, if you feel adventurous, in the draft manual. Both are available from the VCC homepage.
Francois

