An integer that is either -1 or is a valid index for each of the given sequences.

The String.indexOf(String) method is declared as

  class String {
   @IndexOrLow("this") int indexOf(String str) { ... }
  }

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