Package org.checkerframework.checker.index.qual

Annotation Interface HasSubsequence

@Documented @Retention(RUNTIME) @Target(FIELD) public @interface HasSubsequence
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.

See the Checker Framework Manual:
Index Checker

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    String
    from
    The index into this where the subsequence starts.
    String
    subsequence
    An expression that evaluates to the subsequence.
    String
    to
    The index into this, immediately past where the subsequence ends.