-
Notifications
You must be signed in to change notification settings - Fork 62
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
VeriFast incomplete for nonlinear arithmetic #195
Comments
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
I'd recommend proving the following lemmas:
( Once you have |
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 The case split above works because VeriFast knows that |
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! |
Greetings,
I think I found a problem with modulo operations as the assertion in the following program fails:
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.
The text was updated successfully, but these errors were encountered: