The annotated sequence contains a subsequence that is equal to the value of some other expression. This annotation permits the Upper Bound Checker to translate indices for one sequence into indices for the other sequence.

Consider the following example:

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

The above annotations mean that the value of an IntSubArray object is equal to a subsequence of its array field.

These annotations imply the following relationships among @IndexFor annotations:

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

When assigning an array a to array, 4 facts need to be true:

• start is @NonNegative.
• end is @LTEqLengthOf("a").
• start is @LessThan("end + 1").
• the value of this equals array[start..end-1]

The Index Checker verifies the first 3 facts, but always issues a warning because it cannot prove the 4th fact. The programmer should manually verify that the subsequence field is equal to the given subsequence 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.