Invariants make OpenJML unsure about bounded variables

[HansvdLaan]

I'm not sure about this but I'm guessing it's a bug. It could also very well be an error on my part.
(Same goes for the title, I don't exactly know what to call this 'bug')

Consider the following class, it's part of an exercise verifying a way to model money:

public class Amount{
	
	//@ public invariant cents >= -100;
	//@ public invariant cents <= 100;
	
	//@ public invariant euros > 0 ==> cents >= 0;
	//@ public invariant euros < 0 ==> cents <= 0;

	private /*@ spec_public @*/ int cents;

	private /*@ spec_public @*/ int euros;

	//@ requires cents >= -100;
	//@ requires cents <= 100;
	//@ requires euros > 0 ==> cents >= 0;
	//@ requires euros < 0 ==> cents <= 0;
	//@ ensures this.cents >= -100;
	//@ ensures this.cents <= 100;
	//@ ensures this.euros > 0 ==> cents >= 0;
	//@ ensures this.euros < 0 ==> cents <= 0;
	public Amount2(int euros, int cents){
	  this.euros = euros;
	  this.cents = cents;
	}
	
	public /*@ pure @*/ Amount negate(){
	  return new Amount(-euros,-cents);
	}

}

OpenJML says negate is invalid with reason being : 'ex1.Amount.negate(): The prover cannot establish an assertion (Precondition: /home/fmt/eclipse-workspace/JmlTestS4/src/ex1/Amount.java:15: ) in method negate' with line 15 being '//@ requires cents >= -100;

However, the following code is correct:

public class Foo{
	
	//@ public invariant a >= -100;
	//@ public invariant a <= 100;

	private /*@ spec_public @*/ int a;

	//@ requires a >= -100;
	//@ requires a <= 100;
	//@ ensures this.a >= -100;
	//@ ensures this.a <= 100;
	public Foo(int a){
	  this.a = a;
	}
	
	public /*@ pure @*/ Foo negate(){
	  return new Foo(-a);
	}
}

[davidcok]

Hans, 1) A newer version will be more precise about precondition failures 2) In this case, the problem is that ‘euros’ might be Integer.MIN_VALUE, in which case ‘-euros’ is still Integer.MIN_VALUE, and the invariant fails. 3) You are warned about the arithmetic overflow if you use the option -code-math=-safe 4) For some reason, you must have -code-maath=java set. It avoids sometimes annoying messages about arithmetic overflow, but can make situations like this one inscrutable. David

…

On Sep 30, 2017, at 5:39 AM, HansvdLaan ***@***.***> wrote: I'm not sure about this but I'm guessing it's a bug. It could also very well be an error on my part. (Same goes for the title, I don't exactly know what to call this 'bug') Consider the following class, it's part of an exercise verifying a way to model money: public class Amount{ //@ public invariant cents >= -100; //@ public invariant cents <= 100; //@ public invariant euros > 0 ==> cents >= 0; //@ public invariant euros < 0 ==> cents <= 0; private /*@ spec_public @*/ int cents; private /*@ spec_public @*/ int euros; //@ requires cents >= -100; //@ requires cents <= 100; //@ requires euros > 0 ==> cents >= 0; //@ requires euros < 0 ==> cents <= 0; //@ ensures this.cents >= -100; //@ ensures this.cents <= 100; //@ ensures this.euros > 0 ==> cents >= 0; //@ ensures this.euros < 0 ==> cents <= 0; public Amount2(int euros, int cents){ this.euros = euros; this.cents = cents; } public /*@ pure @*/ Amount negate(){ return new Amount(-euros,-cents); } } OpenJML says negate is invalid with reason being : 'ex1.Amount.negate(): The prover cannot establish an assertion (Precondition: /home/fmt/eclipse-workspace/JmlTestS4/src/ex1/Amount.java:15: ) in method negate' with line 15 being '//@ requires cents >= -100; However, the following code is correct: public class Foo{ //@ public invariant a >= -100; //@ public invariant a <= 100; private /*@ spec_public @*/ int a; //@ requires a >= -100; //@ requires a <= 100; //@ ensures this.a >= -100; //@ ensures this.a <= 100; public Foo(int a){ this.a = a; } public /*@ pure @*/ Foo negate(){ return new Foo(-a); } } — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#567>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AFExwOew8PP-RfYqbhja8VBJein1MyG4ks5sngxPgaJpZM4PpgeH>.

[davidcok]

Adding this as a test case, but closing the issue