Addition with LessThan

[kelloggm]

Given a, b, and c are all non-negative integers, and b < c, then we can conclude that a + b < a + c.

Consider the following example from Guava:

    public List<Short> subList(
            @IndexOrHigh("this") @LessThan("#2") int fromIndex,
            @IndexOrHigh("this") int toIndex) {
      int size = size();
      checkPositionIndexes(fromIndex, toIndex, size);
      if (fromIndex == toIndex) {
        return Collections.emptyList();
      }
      return new ShortArrayAsList(array, start + fromIndex, start + toIndex);
    }

The constructor call on the last line requires the second parameter to be less than the third.

[smillst]

I don't think it matters if a, b, or c are non-negative. If b < c then a + b < a + c.

[mernst]

Modulo overflow, of course.

[kelloggm]

You're both right. I think it's worth implementing anyway - the Index Checker is already unsound wrt overflow.