org.checkerframework.checker.index.qual

Annotation Type HasSubsequence

@Target(value=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;
    int @IndexFor("array") int start;
    int @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 start + i is @IndexFor("array").
• If j is @IndexFor("array"), then j - 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 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 and 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.

Element Detail

subsequence

public abstract String subsequence

An expression that evaluates to the subsequence.

from

public abstract String from

The index into this where the subsequence starts.

to

public abstract String to

The index into this, immediately past where the subsequence ends.