VeriFast incomplete for nonlinear arithmetic

[EGeraldo]

Greetings,

I think I found a problem with modulo operations as the assertion in the following program fails:

public class A {
        public void foo(int x)
        //@ requires x == 5;
	//@ ensures true;
	{	
		//@ assert x%10 == 5;
	}
}

Shouldn't the assumption x=5 be taken into account?

One other detail i noticed is that Verifast's modulo does not take the operands sign into consideration, while Java (and C - depending on the implementation) considers the sign of the dividend.

Best regards.

[jpdoyle]

In this case automatically substituting constants is possible, but if you're doing anything more complicated you'll need to be able to prove stuff about %. The general spec of % (at least for C) is:

lemma void div_rem(int D, int d);
    requires d != 0;
    ensures D == D / d * d + D % d &*& abs(D % d) < abs(d) &*& abs(D / d * d) <= abs(D);

I'd recommend proving the following lemmas:

lemma void division_zero_unique(int d, int q, int r);
    requires d != 0 &*& abs(r) < abs(d) &*& 0 == d*q + r;
    ensures  q == (0/d) &*& q == 0 &*& r == (0%d) &*& r == 0;

lemma void division_unique(int D, int d, int q, int r);
    requires d != 0 &*& abs(r) < abs(d) &*& abs(d*q) <= abs(D)
        &*&  D == d*q + r;
    ensures  q == (D/d) &*& r == (D%d);

(division_zero_unique is the tricky half, and division_unique is a pretty easy corollary)

Once you have division_unique, division_unique(x,10,0,5) proves the statement.

[btj]

Hi @EGeraldo. I changed the title because while VeriFast does not simply ignore assumptions, the underlying theorem prover is very incomplete for nonlinear arithmetic, including division and modulo. You generally need to help the theorem prover by inserting ghost statements such as lemma calls, as suggested by jpdoyle.

Sometimes, inserting a case split does the trick:

public class A {
        public void foo(int x)
        //@ requires x == 5;
	//@ ensures true;
	{
		//@ if (x/10 < 0) {} else if (x/10 > 0) {} else {}
		//@ assert x%10 == 5;
	}
}

If you run verifast -c -stats thefile.java on this example, you'll see that VeriFast applies the modulo_nonnegative and modulo_div autolemmas defined in bin/rt/java.lang.javaspec. (That file will be opened in the VeriFast IDE when you run a verification. You can find it by choosing Window (Bottom).)

The case split above works because VeriFast knows that X < 0 for integer X implies X <= 1.

[btj]

About your "other detail": I don't see what exactly you are referring to. If you have a specific example on which VeriFast exhibits incorrect or otherwise undesirable behavior, please open a separate issue. Thanks!