Unsolicited state transition

[rodrigomilisse]

When analising a StateRefinement without a to value, the from value may replace the current information about the state variable used in the from value.

Example

import liquidjava.specification.*;
import java.util.ArrayList;

@ExternalRefinementsFor("java.util.ArrayList")
@Ghost("int x")
public interface TestTransitionsRefinements<E> {
	@StateRefinement(to = "x(this) == 0")
	public abstract void ArrayList();

	@StateRefinement(to = "x(this) == x(old(this)) + 1")
	public abstract void add(E e);

	@StateRefinement(from = "x(this) > 0")
	public abstract E get(int index);

	@StateRefinement(from = "x(this) > 1")
	public abstract E getFirst();

	@StateRefinement(from = "x(this) > 0", to = "x(this) == x(old(this)) - 1")
	public abstract void remove(int index);
}

public class TestTransitions {

	public static void main(String[] args) {
		ArrayList<Integer> list = new ArrayList<>();
		list.add(1);
		list.add(2);

		list.remove(0);
		list.remove(0);

		// ok

		ArrayList<Integer> list2 = new ArrayList<>();
		list2.add(1);
		list2.add(2);
		list2.getFirst();
		list2.remove(0);
		list2.remove(0);

		// ok

		ArrayList<Integer> list3 = new ArrayList<>();
		list3.add(1);
		list3.add(2);
		list3.get(0);
		list3.remove(0);
		list3.remove(0);

		// fail
	}
}

In this case, the detail x(this) == 2 is replaced by x(this) > 0 when calling the get() method. This loss of information means that an error is thrown when trying to call remove() twice because the second remove can no longer guarantee it's pre-condition that x(this) > 0. The first list doen't call a method before the removes, so the information is kept and the second list calls getFirst() with a stronger pre-condition that ensures that at least two calls to remove are possible.

Error Thrown

______________________________________________________
Failed to check state transitions when calling list3.remove(0) in:

list3.remove(0)

Expected possible states:(x(this) > 0)

State found:
----------------------------------------------------------------------------------------------------------------------------------
∀#list3_43:ArrayList, (x(#list3_43) == x(#list3_41) - 1)  => 
∀#list3_41:ArrayList, (x(#list3_41) > 0) 
----------------------------------------------------------------------------------------------------------------------------------

Instance translation table:
----------------------------------------------------------------------------------------------------------------------------------
| Variable Name                    | Created in                                                   | File 
----------------------------------------------------------------------------------------------------------------------------------
| #list3_41                        | list3.get(0)                                                 | TestTransitions.java:47, 3 
| #list3_43                        | list3.remove(0)                                              | TestTransitions.java:48, 3 
----------------------------------------------------------------------------------------------------------------------------------

Location: (/home/rodri/documents/LASIGE/barista/saved/new/TestTransitions.java:49)
______________________________________________________

In summary x(this) == x(old(this)) - 1 && x(old(this)) > 0 instead of x(this) == x(old(this)) - 1 && x(old(this)) == 2

Intended behaviour

StateRefinements without a to value should not affect state

[alcides]

I am not sure about this.

@StateChange(from="state_one(this)")
public void goToRandomState();

This method, which forgets information about which state the object is in is no longer possible to write, correct?

[GUIpsp]

I had a pretty in depth discussion with Márcio where I brought up this point, and the conclusion is that, essentially, LiquidJava is not very logically consistent in handling what states are kept and which are forgotten.

For example, if the behaviour changed to "keep unless mentioned in to", you could make it forget by including a tautology in the to.

But even if the behavior doesn't change, you still have to do something similar if the state you are trying to affect is not part of the from.
For example, if you have a variable tracking the even-ness of a counter, you might have to write something like this in the current implementation:

@StateChange(to="even(this) || !even(this)")
public void goToRandomCount();

which is also not nice