Collection defines retainAll as taking a Collection<?> c parameter, meaning a collection with possibly null elements:
https://github.com/eisop/jdk/blob/a4b7e04c9a6fa0c9451b3064464a46b943fa40a6/src/java.base/share/classes/java/util/Collection.java#L597
Certain subclasses, e.g. LinkedBlockingDeque override that method to take a Collection<? extends @NonNull Object> c parameter, forbidding null values
https://github.com/eisop/jdk/blob/a4b7e04c9a6fa0c9451b3064464a46b943fa40a6/src/java.base/share/classes/java/util/concurrent/LinkedBlockingDeque.java#L1353
This matches the description of the logic of the method but is an unsound covariant change.
eisop/jdk#9 changes the signature to match the overridden method.
Is there a sound way to specify the relation between these methods, without resorting to arbitrary pre-conditions? (In JML one could add a predicate to Collection that decides whether it accepts null. retainAll would have a pre-condition that the predicate of this and c matches (maybe this being "weaker" than c).)
CollectiondefinesretainAllas taking aCollection<?> cparameter, meaning a collection with possibly null elements:https://github.com/eisop/jdk/blob/a4b7e04c9a6fa0c9451b3064464a46b943fa40a6/src/java.base/share/classes/java/util/Collection.java#L597
Certain subclasses, e.g.
LinkedBlockingDequeoverride that method to take aCollection<? extends @NonNull Object> cparameter, forbidding null valueshttps://github.com/eisop/jdk/blob/a4b7e04c9a6fa0c9451b3064464a46b943fa40a6/src/java.base/share/classes/java/util/concurrent/LinkedBlockingDeque.java#L1353
This matches the description of the logic of the method but is an unsound covariant change.
eisop/jdk#9 changes the signature to match the overridden method.
Is there a sound way to specify the relation between these methods, without resorting to arbitrary pre-conditions? (In JML one could add a predicate to Collection that decides whether it accepts null.
retainAllwould have a pre-condition that the predicate ofthisandcmatches (maybethisbeing "weaker" thanc).)