org.checkerframework.checker.index.qual

Annotation Type HasSubsequence

@Target(value=FIELD)
public @interface HasSubsequence

A sequence whose declaration is annotated with this annotation contains a named subsequence. This annotation permits indices for the subsequence to be translated into indices for this sequence and vice-versa.

Consider the following example (note that because this annotation is a declaration annotation, it appears immediately before the declaration of the field - not as the primary type on the array!):

   class IntSubArray {
    @HasSubsequence(value = "this", from = "this.start", to = "this.end") int [] array;
    int  @IndexFor("array") int start;
    int  @IndexOrHigh("array") int end;
   }
 

These annotations allow two kinds of indexing operations that would otherwise be forbidden:

• If i is @IndexFor("this"), then start + i is @IndexFor("array").
• If j is @IndexFor("array"), then j - start is @IndexFor("this").

When assigning an array a to array, 3 facts need to be proven:

• start is @NonNegative.
• end is @LTEqLengthOf("a").
• start is @LessThan("end + 1").

A warning will still be issued at this assignment, because the Index Checker cannot prove that "this" is the name of the subsequence, only that such a subsequence exists. You should manually verify that the named sequence is, in fact, the subsequence described in the annotation and then suppress the warning.

For an example of how this annotation is used in practice, see the test GuavaPrimitives.java in /checker/tests/index/.

This annotation may only be written on fields.

See the Checker Framework Manual:

Index Checker

Required Element Summary

Required Elements

Modifier and Type	Required Element and Description
String	from
String	to
String	value

Element Detail

value

public abstract String value

from

public abstract String from

to

public abstract String to