An integer that, for each of the given sequences, is either a valid index or is equal to the sequence's length.

The Arrays.binarySearch method is declared as

class Arrays {
  int binarySearch(Object[] a, @IndexFor("#1") int fromIndex, @IndexOrHigh("#1") int toIndex, Object key)
}

Writing @IndexOrHigh("arr") is equivalent to writing @NonNegative @LTEqLengthOf("arr"), and that is how it is treated internally by the checker. Thus, if you write an @IndexFor("arr") annotation, you might see warnings about @NonNegative or @LTEqLengthOf.