Preserve State in State Refinements without Postcondition (#191)

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/ArrayListRefinements.java

@@ -0,0 +1,22 @@
+package testSuite.classes.state_refinement_no_to_correct;
+
+import liquidjava.specification.ExternalRefinementsFor;
+import liquidjava.specification.RefinementPredicate;
+import liquidjava.specification.StateRefinement;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+public interface ArrayListRefinements<E> {
+
+    @RefinementPredicate("int size(ArrayList l)")
+    @StateRefinement(to = "size(this) == 0")
+    public void ArrayList();
+
+    @StateRefinement(to = "size(this) == size(old(this)) + 1")
+    public boolean add(E e);
+
+    @StateRefinement(from = "size(this) > 0")
+    public E get(int index);
+
+    @StateRefinement(from = "size(this) == 2", to = "size(this) == size(old(this)) - 1")
+    public E remove(int index);
+}

liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_correct/Test.java

@@ -0,0 +1,13 @@
+package testSuite.classes.state_refinement_no_to_correct;
+
+import java.util.ArrayList;
+
+public class Test {
+    public void example() {
+        ArrayList<Integer> list = new ArrayList<>();
+        list.add(1);
+        list.add(2);
+        list.get(0);
+        list.remove(0);
+    }
+}

liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Counter.java

@@ -0,0 +1,23 @@
+package testSuite.classes.state_refinement_no_to_typestate_correct;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "one", "many"})
+public class Counter {
+
+    @StateRefinement(to="empty(this)")
+    public Counter() {}
+
+    @StateRefinement(from="empty(this)", to="one(this)")
+    public void addFirst() {}
+
+    @StateRefinement(from="one(this)", to="many(this)")
+    public void addSecond() {}
+
+    @StateRefinement(from="one(this) || many(this)")
+    public void inspect() {}
+
+    @StateRefinement(from="many(this)")
+    public void consumeOne() {}
+}

liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Test.java

@@ -0,0 +1,12 @@
+package testSuite.classes.state_refinement_no_to_typestate_correct;
+
+public class Test {
+
+    public void test() {
+        Counter counter = new Counter();
+        counter.addFirst();
+        counter.addSecond();
+        counter.inspect();
+        counter.consumeOne();
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/context/ObjectState.java

@@ -55,7 +55,9 @@ public void setMessage(String message) {
     }
 
     public ObjectState clone() {
-        return new ObjectState(from.clone(), to.clone(), message);
+        Predicate clonedFrom = from == null ? null : from.clone();
+        Predicate clonedTo = to == null ? null : to.clone();
+        return new ObjectState(clonedFrom, clonedTo, message);
     }
 
     @Override

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -182,10 +182,6 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
         if (to != null)
             state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix));
 
-        // has from but not to, state remains the same
-        if (from != null && to == null)
-            state.setTo(createStatePredicate(from, f.getTargetClass(), tc, e, true, prefix));
-
         // has to but not from, state enters with true
         if (from == null && to != null)
             state.setFrom(new Predicate());
@@ -617,4 +613,4 @@ private static List<CtAnnotation<? extends Annotation>> getStateAnnotation(CtEle
                 .getCanonicalName().contentEquals("liquidjava.specification.StateRefinement"))
                 .collect(Collectors.toList());
     }
-}
+}