org.checkerframework.checker.index.qual

Annotation Type LengthOf

@Target(value={TYPE_USE,TYPE_PARAMETER,METHOD})
public @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 and Description
java.lang.String[]	value Sequences that the annotated expression is equal to the length of.

Element Detail

value

public abstract java.lang.String[] value

Sequences that the annotated expression is equal to the length of.