Annotation Interface LengthOf


An integer that, for each of the given sequences, is equal to the sequence's length.

This is treated as an IndexOrHigh annotation internally. This is an implementation detail that may change in the future, when this type may be used to implement more precise refinements.

The usual use case for the LengthOf annotation is in the defintions of custom collections. Consider the signature of java.lang.String#length():


     public @LengthOf("this") int length()
 
See the Checker Framework Manual:
Index Checker
  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    Sequences that the annotated expression is equal to the length of.
  • Element Details

    • value

      String[] value
      Sequences that the annotated expression is equal to the length of.