Fixed-size instances of mutable collections

[kelloggm]

A collection value may be of fixed size even though it has a mutable type. (Or, the value may be of fixed size in the scope in which it is analyzed, such as within a method call to which it is passed as an argument.)

For instance, a method might take a CharSequence and create an index into it by comparing it to CharSequence#length:

void test(CharSequence seq) {
    if (seq.length() > 0) {
        @IndexFor("seq") int index = seq.length() - 1;
    }
}

Currently, the Index Checker forbids this code. This is because CharSequences can be mutable, so the return type of CharSequence#length does not have an upper bound annotation. In this specific case, seq is immutable, so the type of seq.length() could be @IndexOrHigh("seq").

A proposal to remedy this is to add a @FixedSize or @Readonly annotation that can be applied to collections. So, the method above would be annotated:

void test(@FixedSize CharSequence seq) {
    if (seq.length() > 0) {
        @IndexFor("seq") int index = seq.length() - 1;
    }
}

On its own, this annotation does nothing. The annotation is trusted.

In CharSequence, we would then annotate the length method so that if the collection is @FixedSize, length returns @IndexOrHigh, using something like @EnsuresQualifierIf (although the actual syntax would likely have to be different):

interface CharSequence {
    @NonNegative @IfFixedSize(LTEqLengthOf.class) int length();
}

Then, we can implicitly add the @FixedSize annotation to known fixed-size implementations of CharSequence, such as String.

[kelloggm]

This is distinct from #154 in that this issue refers to specific fixed-size instances of collections that are generally mutable. Issue #154 refers to classes that are always immutable.