runtimeverification / javamop

Runtime verification system for Java, using AspectJ for instrumentation.
http://fsl.cs.illinois.edu/javamop
MIT License
45 stars 37 forks source link

Improvement of Iterator_RemoveOnce #238

Open emopers opened 8 years ago

emopers commented 8 years ago

For property Iterator_RemoveOnce, we noticed that it would give false alarms on ListIterator if the ListIterator used previous() to move the iterator. Following is one snippet illustrating how JavaMOP can raise alarms while the program is legal:

import java.util.ArrayList;
import java.util.ListIterator;

public class Iterator_RemoveOnce {
    public static void main(String[] args) {
        ArrayList<Integer> arr = new ArrayList<Integer>();
        for(int i = 0; i < 10; i++) {
            arr.add(i);
        }
        ListIterator<Integer> it = arr.listIterator(arr.size());
        while(it.hasPrevious()) {
            it.previous();
            it.remove();
        }
    }
}

This operation is allowed in property ListIterator_RemoveOnce, but as ListIterator is a subclass of Iterator, it is still considered illegal by Iterator_RemoveOnce. We suggest to have Iterator_RemoveOnce property to exclude ListIterator, as there is already a good property specifically for it.