checker/tests/index/LessThanCustomCollection.java

package lessthan;

import org.checkerframework.checker.index.qual.IndexFor;
import org.checkerframework.checker.index.qual.IndexOrHigh;
import org.checkerframework.checker.index.qual.IndexOrLow;
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.checker.index.qual.LengthOf;
import org.checkerframework.checker.index.qual.LessThan;
import org.checkerframework.checker.index.qual.NonNegative;
import org.checkerframework.dataflow.qual.Pure;

// This class has a similar implementation to several Immutable*Array class in Guava,
// such as com.google.common.primitives.ImmutableDoubleArray.
public class LessThanCustomCollection {
  // This object is a subset of array. So, if something is an index for "this"
  // then it is >= start and < end.
  private final int[] array;
  private final @IndexOrHigh("array") @LessThan("end + 1") int start;
  private final @LTLengthOf(
      value = {"array", "this"},
      offset = {" - 1", "- start"}) int end;

  private LessThanCustomCollection(int[] array) {
    this(array, 0, array.length);
  }

  private LessThanCustomCollection(
      int[] array, @IndexOrHigh("#1") @LessThan("#3 + 1") int start, @IndexOrHigh("#1") int end) {
    this.array = array;
    // can't est. that end - start is the length of this.
    // :: error: (assignment)
    this.end = end;
    // start is @LessThan(end + 1) but should be @LessThan(this.end + 1)
    // :: error: (assignment)
    this.start = start;
  }

  @Pure
  public @LengthOf("this") int length() {
    return end - start;
  }

  public double get(@IndexFor("this") int index) {
    // TODO: This is a bug.
    // :: error: (argument)
    checkElementIndex(index, length());
    // Because index is an index for "this" the index + start
    // must be an index for array.
    // :: error: (array.access.unsafe.high)
    return array[start + index];
  }

  public static @NonNegative int checkElementIndex(
      @LessThan("#2") @NonNegative int index, @NonNegative int size) {
    if (index < 0 || index >= size) {
      throw new IndexOutOfBoundsException();
    }
    return index;
  }

  public @IndexOrLow("this") int indexOf(double target) {
    for (int i = start; i < end; i++) {
      if (areEqual(array[i], target)) {
        // Don't know that is is greater than start.
        // :: error: (return)
        return i - start;
      }
    }
    return -1;
  }

  static boolean areEqual(int item, double target) {
    // implementation not relevant
    return true;
  }
}