The Checker Framework Manual:
Custom pluggable types for Java

Chapter 22 Modifiability Checker

In the Java Collections Framework, an optional method is one that a class may or may not support. If a method is unsupported, calling it throws UnsupportedOperationException. The Modifiability Checker verifies that optional methods related to modifying collections are only called if they are supported, thus eliminating the possibility of an UnsupportedOperationException at run time. (It is possible to write a checker that warns about other unsupported methods, but the Modifiability Checker focuses on those issued when modifying collections.)

An example of an optional method is add. Some subclasses of Collection support add, and others (such as the result of calling Collections.unmodifiableCollection) do not support add.

If the Modifiability Checker issues no warning, then your program is guaranteed not to throw UnsupportedOperationException due to invoking an optional method (such as add or remove) on an unmodifiable collection. (For brevity, this chapter generally uses just “collection” to mean “collection, map, or iterator”.)

In addition to preventing UOEs, the Modifiability Checker ensures that collections that the user intends to be unmodifiable have an unmodifiable run-time implementation.

To run the Modifiability Checker:

javac -processor org.checkerframework.checker.modifiability.ModifiabilityChecker MyFile.java

22.1 Unmodifiable collections

An unmodifiable collection is one that throws UnsupportedOperationException if a mutating method is called. The JDK provides many such collections, for example, the results of:

• • List.of(), List.copyOf()

• • Set.of(), Set.copyOf()

• • Map.of(), Map.copyOf()

• • Collections.emptyList(), Collections.emptySet(), Collections.emptyMap()

• • Collections.unmodifiableList(), Collections.unmodifiableSet(), Collections.unmodifiableMap()

A modifiable collection supports calling at least one optional mutating method. In general, classes support groups of methods which correspond to four different ways a collection can be modified. A collection may support modifying a collection through one or more of the capabilities Grow, Sequential Grow, Shrink, and Replace.

• • Grow: The collection can grow by adding new elements (add, addAll, offer, …) at arbitrary locations. Not to be confused with sequential grow.

• • Sequential Grow: The sequenced collection can grow by adding new elements at the beginning or end (addFirst, addLast, offerFirst, offerLast, push, putFirst, putLast, …).

  The Sequential Grow capability is needed for collections, such as TreeSet, that support grow operations (like add and addAll) but do not support sequential grow operations (like addFirst and addLast). The declaration of TreeSet is annotated as @Growable @SeqUngrowable.

  “Sequential Grow” is shortened to “SeqGrow” in the rest of the manual.

• • Shrink: The collection can shrink by removing existing elements (remove, removeAll, clear, retainAll, poll, pop, …).

• • Replace: The collection can replace existing elements with new values at specific locations/keys (List.set, Map.replace, Map.replaceAll, ListIterator.set, Collections.sort, Map.Entry.setValue, …).

Some collections can also be modified through their iterator; see Section 22.4.

The following table summarizes the main method families that may be called for each capability. It is not a list of every overload. Read-only methods such as get, contains, size, isEmpty, iterator, and entrySet do not require a modifiability capability.

An overriding method must preserve positive modifiability receiver requirements exactly. For example, if a superclass method has a @Growable, @SeqGrowable, @Shrinkable, or @Replaceable receiver, then the overriding method must require that same positive receiver capability; it may not drop or weaken the requirement.

22.2 Modifiability annotations

The Modifiability Checker uses multiple independent 4-element hierarchies, one per capability. Every collection type carries exactly one qualifier from each hierarchy. The checker also uses an additional 2-element hierarchy to express whether a collection’s iterator preserves the collection’s capabilities: whether remove() can be called on the iterator, and, for a ListIterator, whether add() and set() can be called.

  Grow hierarchy              SeqGrow hierarchy                Shrink hierarchy                 Replace hierarchy                   Iterator hierarchy

    @MaybeGrowable            @MaybeSeqGrowable             @MaybeShrinkable                  @MaybeReplaceable              @MaybeIteratorPolyMod
      /      \                   /       \                        /       \                       /       \                             |
 @Growable @Ungrowable     @SeqGrowable @SeqUngrowable      @Shrinkable @Unshrinkable      @Replaceable @Unreplaceable                  |
      \      /                   \       /                        \       /                       \       /                             |
    @BottomGrowable          @BottomSeqGrowable              @BottomShrinkable                 @BottomReplaceable               @IteratorPolyMod

Figure 22.1 shows the hierarchies. Each hierarchy is type-checked individually. An assignment T x = y is valid only if the compile-time type of y is a subtype of (or equal to) T in every hierarchy simultaneously. For example, @Growable @MaybeSeqGrowable @MaybeShrinkable @MaybeReplaceable List is a subtype of @MaybeGrowable @MaybeSeqGrowable @MaybeShrinkable @MaybeReplaceable List (because @Growable @MaybeGrowable), but it is not a subtype of @Ungrowable @MaybeSeqGrowable @MaybeShrinkable @MaybeReplaceable List (because @Growable and @Ungrowable are incomparable siblings in the Grow hierarchy).

22.2.1 Alias annotations

For convenience, the Modifiability Checker provides five alias annotations. They are not part of any hierarchy; the checker expands each one into its constituent qualifiers when it appears in source code.

@Modifiable

Alias for @Growable @SeqGrowable @Shrinkable @Replaceable (but see Section 22.3 for exceptions). Calling any mutating operation on this collection will not throw UnsupportedOperationException.

@Unmodifiable

Alias for @Ungrowable @SeqUngrowable @Unshrinkable @Unreplaceable (but see Section 22.3 for exceptions). The collection is definitely unmodifiable: calling any mutating operation always throws UnsupportedOperationException. The checker issues a warning at every invocation of a grow, seq-grow, shrink, or replace operation.

@MaybeModifiable

Alias for @MaybeGrowable @MaybeSeqGrowable @MaybeShrinkable @MaybeReplaceable. The checker cannot determine the modifiability of the collection. The checker conservatively issues a warning at every invocation of a grow, seq-grow, shrink, or replace operation.

@UnmodifiableParam

Syntactic sugar for @MaybeModifiable. It may only be written within a formal parameter type to indicate that the method does not modify the parameter. This annotation (and @MaybeModifiable) enable the programmer to distinguish between a data structure’s capability to perform a modification and the programmer’s intent about whether a modification should occur. @UnmodifiableParam may appear nested within a parameter type, such as in List<@UnmodifiableParam List<String>>.

@UnmodifiableParam represents reference unmodifiability: no modification may happen through the reference, but an alias may modify the value. By contrast, @Unmodifiable is object unmodifiability: no alias may modify the value.

@PolyModifiable

Alias for @PolyGrowable @PolySeqGrowable @PolyShrinkable @PolyReplaceable (see Section 22.2.3).

Examples using alias annotations:

    @Modifiable List<String> mod = new ArrayList<>(); // all four capabilities
    @Unmodifiable List<String> unmod = List.of("a");   // no capabilities
    @MaybeModifiable List<String> unknown = ...; // capabilities are unknown at compile time
    void foo(@UnmodifiableParam List<String> list) { ... } // foo does not modify list

22.2.2 Qualifiers

The Grow hierarchy

@MaybeGrowable

The top qualifier in the Grow hierarchy. The checker cannot determine whether this collection supports grow operations. Calling grow operations such as add, addAll, etc. on this collection may throw UnsupportedOperationException. This is the default qualifier for unannotated types in the Grow hierarchy.

@Growable

Calling grow operations such as add, addAll, etc. on this collection will not throw UnsupportedOperationException.

@Ungrowable

Calling grow operations such as add, addAll, etc. on this collection will throw UnsupportedOperationException.

@BottomGrowable

The bottom qualifier in the Grow hierarchy. Programmers should rarely write it.

The SeqGrow hierarchy

@MaybeSeqGrowable

The top qualifier in the SeqGrow hierarchy. The checker cannot determine whether this collection or map supports sequenced grow operations. Calling sequenced grow operations such as addFirst, addLast, putFirst, and putLast on this collection or map may throw UnsupportedOperationException. This is the default qualifier for unannotated types in the SeqGrow hierarchy.

@SeqGrowable

Sequenced grow operations, such as addFirst and addLast for collections or putFirst and putLast for maps, will not throw UnsupportedOperationException.

@SeqUngrowable

Sequenced grow operations, such as addFirst and addLast for collections or putFirst and putLast for maps, will throw UnsupportedOperationException. For example, TreeSet and ConcurrentSkipListSet support ordinary add but throw UnsupportedOperationException for explicit positional insertion with addFirst and addLast. Similarly, TreeMap and ConcurrentSkipListMap support ordinary put but throw UnsupportedOperationException for explicit positional updates with putFirst and putLast.

@BottomSeqGrowable

The bottom qualifier in the SeqGrow hierarchy. Programmers should rarely write it.

The Shrink hierarchy

@MaybeShrinkable

The top qualifier in the Shrink hierarchy. The checker cannot determine whether this collection supports shrink operations. Calling shrink operations such as remove, clear, etc. on this collection may throw UnsupportedOperationException. This is the default qualifier for unannotated types in the Shrink hierarchy.

@Shrinkable

Calling shrink operations such as remove, clear, etc. on this collection will not throw UnsupportedOperationException.

@Unshrinkable

Calling shrink operations such as remove, clear, etc. on this collection will throw UnsupportedOperationException.

@BottomShrinkable

The bottom qualifier in the Shrink hierarchy. Programmers should rarely write it.

The Replace hierarchy

@MaybeReplaceable

The top qualifier in the Replace hierarchy. The checker cannot determine whether this collection supports replace operations. Calling replace operations such as set, replaceAll, etc. on this collection may throw UnsupportedOperationException. This is the default qualifier for unannotated types in the Replace hierarchy.

@Replaceable

Calling replace operations such as set, replaceAll, etc. on this collection will not throw UnsupportedOperationException.

@Unreplaceable

Calling replace operations such as set, replaceAll, etc. on this collection will throw UnsupportedOperationException.

@BottomReplaceable

The bottom qualifier in the Replace hierarchy. Programmers should rarely write it.

The Iterator hierarchy

@MaybeIteratorPolyMod

The top qualifier. The checker cannot determine whether this collection’s iterator() is @PolyShrinkable. This is the default qualifier for unannotated types.

@IteratorPolyMod

This collection’s iterator() is @PolyShrinkable. That is, if collection c is @Shrinkable, then c.iterator() is also @Shrinkable.

It might seem that it is sufficient to simply annotate iterator() directly, as in

class List {
  @MaybeShrinkable Iterator iterator() { ... }
}
class ArrayList {
  @PolyShrinkable Iterator iterator(@PolyShrinkable ArrayList this) { ... }
}
class CopyOnWriteArrayList {
  @Unshrinkable Iterator iterator(@PolyShrinkable CopyOnWriteArrayList this) { ... }
}

That approach would be sound but imprecise. In practice, many expressions of static type List evaluate to ArrayLists or other classes with @PolyShrinkable iterator() methods. The @IteratorPolyMod annotation is similar to writing the hypothetical annotation @RuntimeType("ArrayList"): it indicates a property that is more precise than the declared type.

22.2.3 Polymorphic qualifiers

A polymorphic qualifier (Section 32.2) specifies that a method’s return type has the same qualifier (in some hierarchy) as a formal parameter type (possibly the receiver).

@PolyGrowable

Polymorphic qualifier for the Grow hierarchy. The return type’s growability matches the growability of whichever formal parameter is annotated with @PolyGrowable.

@PolySeqGrowable

Polymorphic qualifier for the SeqGrow hierarchy. The return type’s seq-growability matches the seq-growability of whichever formal parameter is annotated with @PolySeqGrowable.

@PolyShrinkable

Polymorphic qualifier for the Shrink hierarchy. The return type’s shrinkability qualifier matches the shrinkability of whichever formal parameter is annotated with @PolyShrinkable. Useful for methods such as Map.keySet() that preserve shrinkability while returning an @Ungrowable view.

@PolyReplaceable

Polymorphic qualifier for the Replace hierarchy. The return type’s replaceability matches the replaceability of whichever formal parameter is annotated with @PolyReplaceable.

@PolyIteratorPolyMod

Polymorphic qualifier for the Iterator hierarchy. The return type’s iterator-preservation qualifier matches the iterator-preservation qualifier of whichever formal parameter is annotated with @PolyIteratorPolyMod.

@PolyModifiable

Alias for @PolyGrowable @PolySeqGrowable @PolyShrinkable @PolyReplaceable. Preserves all four capabilities simultaneously. Use on methods such as Collections.synchronizedList that do not change modifiability.

22.2.4 Modifiability method annotations

The Modifiability Checker supports method annotations that specify method behavior.

@PreservesModifiability

Indicates that if the argument to the method is modifiable, then the returned collection is also modifiable. However, if the argument is unmodifiable, then the returned collection may or may not be unmodifiable. This is useful for methods that may return their argument, or may return a new modifiable collection. For example, if the argument is @Growable, then the returned collection is also @Growable. But if the argument is @Ungrowable, then the return collection is @MaybeGrowable. More generally, if the argument is @Growable, @Shrinkable, @Replaceable, @SeqGrowable, or @IteratorPolyMod, then the Modifiability Checker treats the return value as having that same capability. If the argument has any other qualifier, the return type is the top qualifier (@MaybeGrowable, @MaybeSeqGrowable, @MaybeShrinkable, @MaybeReplaceable, or @MaybeIteratorPolyMod) in the corresponding hierarchy.

This annotation may only be written on non-void, one-argument method declarations. The formal parameter may not be a varargs parameter, because the first argument of a call to a varargs method is an element of the varargs array rather than the sole formal parameter.

@ThrowsUnsupportedOperation

Indicates that the method’s implementation always throws UnsupportedOperationException. Write it on a skeletal implementation, such as one in java.util.AbstractList, that a subclass is expected to override.

A subclass that inherits the implementation, without overriding it, does not support the operation, even if the subclass declares that it does. The Modifiability Checker issues an error for such a subclass; see Section 22.2.5. Without the annotation, it could not, because the body of an inherited method is compiled separately and the checker sees only its signature.

The Modifiability Checker verifies the annotation on every method that it compiles: the body must be exactly throw new UnsupportedOperationException(...).

Do not write the annotation on a method that throws UnsupportedOperationException only because some other method does, such as AbstractList.add(E), whose body is add(size(), e). A subclass that overrides the other method makes such a method work.

22.2.5 Inherited implementations

The Modifiability Checker requires the constructors of a class to agree with the class’s method bodies: if the constructors are @Ungrowable, then every method with a @Growable receiver must throw UnsupportedOperationException, and if the constructors are @Growable, then no such method may.

A class does not escape the requirement by inheriting a method rather than declaring it. For example, this class does not support add(), because AbstractList implements add(int, E) by throwing UnsupportedOperationException:

    // error: the inherited implementation of add(int, E) throws
    class GrowableList extends AbstractList<String> {
      @Growable GrowableList() {}
      ...
    }

The checker knows that an inherited implementation throws UnsupportedOperationException if the method is annotated @ThrowsUnsupportedOperation, or if the method’s class declares the negative qualifier on its constructors, in which case the checker already verified that the method throws. The checker cannot tell for any other inherited method, so it says nothing about one.

22.3 @Modifiable and @Unmodifiable for types without grow, seq-grow, shrink, and/or replace methods

Ordinarily, the declaration @Modifiable MyClass x; is equivalent to @Growable @SeqGrowable @Shrinkable @Replaceable MyClass x;, and @Unmodifiable MyClass x; is equivalent to @Ungrowable @SeqUngrowable @Unshrinkable @Unreplaceable MyClass x;.

However, some types lack methods for one or more mutation capabilities. In such cases, the Modifiability Checker weakens the structurally unavailable component to the corresponding top qualifier. For example, Iterator has remove but not add or set, so @Modifiable Iterator expands to @MaybeGrowable @MaybeSeqGrowable @Shrinkable @MaybeReplaceable Iterator.

22.3.1 Alternative design: use negative capability rather than top qualifier

An alternative design would make Modifiable Iterator expand to @Ungrowable @Shrinkable @Unreplaceable Iterator. That would be incorrect, because not every Iterator is @Ungrowable and @Unreplaceable. For example, the static type Iterator does not declare add or set (they are structurally unavailable), but its subtype ListIterator and does declare those methods. Therefore @Modifiable Iterator should not mean that every iterator is incapable of grow and replace; it means only that those capabilities are not known from the static type Iterator.

Similarly, Queue does not declare replacement methods, but a variable with declared type Queue may contain a LinkedList, which does support replacement operations.

Using the top qualifier for structurally unavailable methods ensures that code like this type-checks:

@Replaceable LinkedList list = ...;
Queue q = list;
@Replaceable LinkedList list2 = (LinkedList) q; // still @Replaceable

22.3.2 Expansion rules for @Modifiable and @Unmodifiable

The following rules define this weakening. A capability is weakened to the corresponding @Maybe* qualifier when the type satisfies that capability’s condition in the table below. For every other type, @Modifiable expands to the capability’s positive qualifier, such as @Growable, and @Unmodifiable expands to the capability’s negative qualifier, such as @Ungrowable.

Weakening conditions for @Modifiable/@Unmodifiable. “” means set difference. A type includes its subtypes.
	Expands to @Maybe*
Grow	Map.Entry or (IteratorListIterator)
SeqGrow	not SequencedCollection, SequencedMap, or Deque
Shrink	Map.Entry
Replace	exact Collection, any Set, (QueueLinkedList),
	or (IteratorListIterator)

These rules describe alias expansion, not the full specification of every JDK type. The JDK annotations may still give a more precise capability for a particular declaration. For instance, SortedSet is a SequencedCollection and SortedMap is a SequencedMap, so their seq-grow component is structurally relevant and is not weakened to @MaybeSeqGrowable. Their JDK declarations are annotated @SeqUngrowable, because their positional insertion methods such as addFirst, addLast, putFirst, and putLast always throw UnsupportedOperationException.

22.3.3 Example expansions for @Modifiable and @Unmodifiable

The following are representative canonical expansions.

22.3.4 Expansion rules for @PolyModifiable

@PolyModifiable is weakened in only one case: on Map.Entry, its grow, seq-grow, and shrink components are the corresponding @Maybe* qualifiers, because no Map.Entry has methods for those capabilities. Every other type keeps all four polymorphic qualifiers, even a type such as Iterator or Queue whose @Modifiable expansion is weakened, because a variable of such a type may hold a value of a subtype, such as ListIterator or LinkedList, that does have the methods.

22.4 Behavior of the iterator() method

By default, the signature of Collection.iterator() is

@MaybeShrinkable Iterator iterator()

However, for some subclasses of Collection, the signature of iterator() is

@PolyShrinkable Iterator iterator(@PolyShrinkable MySubclassOfCollection this)

A collection uses the second signature if the collection is @IteratorPolyMod. The collection uses the first signature if the collection is @MaybeIteratorPolyMod.

Here are examples of its use:

    @IteratorPolyMod @Shrinkable List<String> list = ...;
    @Shrinkable Iterator<String> it = list.iterator();
    it.remove(); // OK

    @IteratorPolyMod @Unshrinkable List<String> list2 = ...;
    @Unshrinkable Iterator<String> it2 = list2.iterator();
    it2.remove(); // Error: it2 is @Unshrinkable

    @Shrinkable List<String> list3 = ...;
    @MaybeShrinkable Iterator<String> it3 = list3.iterator();
    it3.remove(); // Error: list3 does not have @IteratorPolyMod

22.5 Examples of Modifiability Checker warnings

import java.util.*;
import org.checkerframework.checker.modifiability.qual.*;

class Demo {

    void basicUsage() {
      // @Modifiable is an alias for @Growable @SeqGrowable @Shrinkable @Replaceable
      @Modifiable List<String> mod = new ArrayList<>();
      mod.add("a");     // OK: @Growable guarantees add() works
      mod.addFirst("z"); // OK: @SeqGrowable guarantees addFirst() works
      mod.remove("a"); // OK: @Shrinkable guarantees remove() works
      mod.set(0, "b"); // OK: @Replaceable guarantees set() works

        // @Unmodifiable is an alias for @Ungrowable @SeqUngrowable @Unshrinkable @Unreplaceable
        @Unmodifiable List<String> unmod = List.of("a", "b");
        unmod.add("c");   // Error: add() requires @Growable, got @Ungrowable
        unmod.addFirst("d"); // Error: addFirst() requires @SeqGrowable, got @SeqUngrowable
        unmod.get(0);     // OK: read-only access needs no capability
    }

    void fineGrainedPermissions(@Growable List<String> g,
                                @Shrinkable List<String> s,
                                @Replaceable List<String> r) {
      // Growable list allows adding elements
      g.add("a");       // OK
      g.remove("a");    // Error: remove() requires @Shrinkable
      g.set(0, "b");    // Error: set() requires @Replaceable

        // Shrinkable list allows removing elements
        s.remove("a");    // OK
        s.add("a");       // Error: add() requires @Growable

        // Replaceable list allows updating elements
        r.set(0, "b");    // OK
        r.add("b");       // Error: add() requires @Growable
    }

    void combinedPermissions(@Growable @Replaceable Map<String, String> map) {
      // Map.put requires both Grow and Replace capabilities
      map.put("key", "value"); // OK

        // Map.remove requires Shrink capability
        map.remove("key");        // Error: @MaybeShrinkable (default) !<: @Shrinkable
    }

    // @PolyModifiable preserves all four capabilities
    @PolyModifiable List<String> wrap(@PolyModifiable List<String> list) {
      return list;
    }

    void testPoly(@Modifiable List<String> mod, @Growable @Shrinkable List<String> gs) {
      @Modifiable List<String> m = wrap(mod);            // OK
      @Growable @Shrinkable List<String> gs2 = wrap(gs); // OK
      // :: error: [assignment]
      @Modifiable List<String> bad = wrap(gs); // Error: gs has @MaybeSeqGrowable and @MaybeReplaceable
    }
}