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
|
import org.checkerframework.checker.index.qual.LTLengthOf;
import org.checkerframework.common.value.qual.MinLen;
// @skip-test until the type system is enriched so it can express either
// * N = Grid.length and N-1 = Grid.length-1, or
// * i < N and i <= N-1
public class SubtractionIndex {
// Version without annotations
public static void main(String[] args) {
int N = 8;
int[] grid = new int[N];
for (int i = 0; i < N; i++) {
System.out.println(grid[(N - 1) - i]);
}
}
// Version with annotations
public static void mainAnnotated(String[] args) {
int N = 8;
int @MinLen(8) [] grid = new int[N];
@SuppressWarnings("upperbound")
@LTLengthOf("grid") int zero = 0;
for (@LTLengthOf("grid") int i = zero; i < N; i++) {
System.out.println(grid[(N - 1) - i]);
System.out.println(grid[(N - i)]);
System.out.println(grid[(N - i) - 1]);
}
}
}
|
