| 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; |
| } |
| } |