1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
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.type.incompatible)
this.end = end;
// start is @LessThan(end + 1) but should be @LessThan(this.end + 1)
// :: error: (assignment.type.incompatible)
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.type.incompatible)
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.type.incompatible)
return i - start;
}
}
return -1;
}
static boolean areEqual(int item, double target) {
// implementation not relevant
return true;
}
}
|
