0
# Index and Bounds Annotations
1

2
Index and bounds checking annotations prevent array bounds exceptions and index-related errors through static analysis. These annotations track relationships between indices, array lengths, and numeric bounds to ensure safe array access.
3

4
## Capabilities
5

6
### Index Validity Annotations
7

8
Annotations that specify valid indices for arrays and collections.
9

10
```java { .api }
11
/**
12
 * Indicates that the annotated expression is a valid index for the specified arrays
13
 */
14
@Documented
15
@Retention(RetentionPolicy.RUNTIME)
16
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
17
@SubtypeOf(LowerBoundUnknown.class)
18
public @interface IndexFor {
19
    String[] value();
20
}
21

22
/**
23
 * Valid index or the length of specified arrays (useful for insertion operations)
24
 */
25
@Documented
26
@Retention(RetentionPolicy.RUNTIME)
27
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
28
@SubtypeOf(UpperBoundUnknown.class)
29
public @interface IndexOrHigh {
30
    String[] value();
31
}
32

33
/**
34
 * Valid index or -1 for specified arrays (useful for search operations)
35
 */
36
@Documented
37
@Retention(RetentionPolicy.RUNTIME)
38
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
39
@SubtypeOf(LowerBoundUnknown.class)
40
public @interface IndexOrLow {
41
    String[] value();
42
}
43
```
44

45
**Usage Examples:**
46

47
```java
48
import org.checkerframework.checker.index.qual.*;
49

50
public class IndexExample {
51
    public void processArray(int[] array, @IndexFor("#1") int index) {
52
        System.out.println(array[index]); // Safe - index is valid for array
53
    }
54
    
55
    public void insertAt(int[] array, @IndexOrHigh("#1") int position, int value) {
56
        // Can insert at any valid index or at the end (position == array.length)
57
        if (position < array.length) {
58
            array[position] = value; // Safe insertion
59
        }
60
    }
61
    
62
    public @IndexOrLow("#1") int find(int[] array, int target) {
63
        for (int i = 0; i < array.length; i++) {
64
            if (array[i] == target) {
65
                return i; // Returns valid index
66
            }
67
        }
68
        return -1; // Returns -1 if not found
69
    }
70
}
71
```
72

73
### Numeric Range Annotations
74

75
Annotations for specifying numeric ranges and constraints.
76

77
```java { .api }
78
/**
79
 * Indicates that the annotated expression evaluates to an integer >= 0
80
 */
81
@Documented
82
@Retention(RetentionPolicy.RUNTIME)
83
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
84
@SubtypeOf(GTENegativeOne.class)
85
public @interface NonNegative {}
86

87
/**
88
 * Indicates that the annotated expression evaluates to an integer > 0
89
 */
90
@Documented
91
@Retention(RetentionPolicy.RUNTIME)
92
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
93
@SubtypeOf(NonNegative.class)
94
public @interface Positive {}
95

96
/**
97
 * Indicates that the annotated expression evaluates to an integer >= -1
98
 */
99
@Documented
100
@Retention(RetentionPolicy.RUNTIME)
101
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
102
@SubtypeOf(LowerBoundUnknown.class)
103
public @interface GTENegativeOne {}
104
```
105

106
**Usage Examples:**
107

108
```java
109
import org.checkerframework.checker.index.qual.*;
110

111
public class RangeExample {
112
    // Array size must be non-negative
113
    public int[] createArray(@NonNegative int size) {
114
        return new int[size]; // Safe - size >= 0
115
    }
116
    
117
    // Count must be positive for meaningful operations
118
    public void repeat(@Positive int count, Runnable action) {
119
        for (int i = 0; i < count; i++) {
120
            action.run();
121
        }
122
    }
123
    
124
    // Search result: valid index or -1
125
    public @GTENegativeOne int binarySearch(int[] array, int target) {
126
        // Implementation returns valid index or -1
127
        return java.util.Arrays.binarySearch(array, target);
128
    }
129
}
130
```
131

132
### Length Relationship Annotations
133

134
Annotations that express relationships between array lengths and indices.
135

136
```java { .api }
137
/**
138
 * Indicates arrays have the same length
139
 */
140
@Documented
141
@Retention(RetentionPolicy.RUNTIME)
142
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
143
@SubtypeOf(SameLenUnknown.class)
144
public @interface SameLen {
145
    String[] value();
146
}
147

148
/**
149
 * Expression is the length of specified arrays
150
 */
151
@Documented
152
@Retention(RetentionPolicy.RUNTIME)
153
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
154
@SubtypeOf(UpperBoundUnknown.class)
155
public @interface LengthOf {
156
    String[] value();
157
}
158

159
/**
160
 * Expression is less than the length of specified arrays
161
 */
162
@Documented
163
@Retention(RetentionPolicy.RUNTIME)
164
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
165
@SubtypeOf(LTEqLengthOf.class)
166
public @interface LTLengthOf {
167
    String[] value();
168
}
169

170
/**
171
 * Expression is less than or equal to the length of specified arrays
172
 */
173
@Documented
174
@Retention(RetentionPolicy.RUNTIME)
175
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
176
@SubtypeOf(UpperBoundUnknown.class)
177
public @interface LTEqLengthOf {
178
    String[] value();
179
}
180

181
/**
182
 * Expression is less than the length minus one of specified arrays
183
 */
184
@Documented
185
@Retention(RetentionPolicy.RUNTIME)
186
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
187
@SubtypeOf(LTLengthOf.class)
188
public @interface LTOMLengthOf {
189
    String[] value();
190
}
191
```
192

193
**Usage Examples:**
194

195
```java
196
import org.checkerframework.checker.index.qual.*;
197

198
public class LengthExample {
199
    // Process arrays of same length
200
    public void processParallel(@SameLen("#2") int[] array1, int[] array2) {
201
        for (int i = 0; i < array1.length; i++) {
202
            // Safe - arrays have same length
203
            System.out.println(array1[i] + array2[i]);
204
        }
205
    }
206
    
207
    // Size parameter represents array length
208
    public void processWithSize(int[] array, @LengthOf("#1") int size) {
209
        for (int i = 0; i < size; i++) {
210
            System.out.println(array[i]); // Safe - i < size == array.length
211
        }
212
    }
213
    
214
    // Index is less than array length
215
    public void safeAccess(int[] array, @LTLengthOf("#1") int index) {
216
        System.out.println(array[index]); // Safe - index < array.length
217
    }
218
}
219
```
220

221
### Search and Substring Operations
222

223
Specialized annotations for search operations and string manipulation.
224

225
```java { .api }
226
/**
227
 * Result of a search operation: valid index or -1
228
 */
229
@Documented
230
@Retention(RetentionPolicy.RUNTIME)
231
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
232
@SubtypeOf(SearchIndexUnknown.class)
233
public @interface SearchIndexFor {
234
    String[] value();
235
}
236

237
/**
238
 * Result of substring operations
239
 */
240
@Documented
241
@Retention(RetentionPolicy.RUNTIME)
242
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
243
@SubtypeOf(SubstringIndexUnknown.class)
244
public @interface SubstringIndexFor {
245
    String[] value();
246
}
247

248
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
249
@SubtypeOf(SearchIndexFor.class)
250
public @interface SearchIndexBottom {}
251

252
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
253
@DefaultQualifierInHierarchy
254
public @interface SearchIndexUnknown {}
255

256
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
257
@SubtypeOf(SubstringIndexFor.class)
258
public @interface SubstringIndexBottom {}
259

260
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
261
@DefaultQualifierInHierarchy
262
public @interface SubstringIndexUnknown {}
263
```
264

265
**Usage Examples:**
266

267
```java
268
import org.checkerframework.checker.index.qual.*;
269

270
public class SearchExample {
271
    public @SearchIndexFor("#1") int findValue(int[] array, int target) {
272
        for (int i = 0; i < array.length; i++) {
273
            if (array[i] == target) {
274
                return i;
275
            }
276
        }
277
        return -1;
278
    }
279
    
280
    public @SubstringIndexFor("#1") int findSubstring(String text, String pattern) {
281
        return text.indexOf(pattern); // Returns valid index or -1
282
    }
283
    
284
    public void useSearchResult(String text, String pattern) {
285
        @SubstringIndexFor("text") int index = findSubstring(text, pattern);
286
        if (index >= 0) {
287
            // Safe to use index for substring operations
288
            String found = text.substring(index, index + pattern.length());
289
            System.out.println("Found: " + found);
290
        }
291
    }
292
}
293
```
294

295
### Comparison and Ordering Annotations
296

297
Annotations for expressing ordering relationships between expressions.
298

299
```java { .api }
300
/**
301
 * Expression is less than the specified expressions
302
 */
303
@Documented
304
@Retention(RetentionPolicy.RUNTIME)
305
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
306
@SubtypeOf(LessThanUnknown.class)
307
public @interface LessThan {
308
    String[] value();
309
}
310

311
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
312
@SubtypeOf(LessThan.class)
313
public @interface LessThanBottom {}
314

315
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
316
@DefaultQualifierInHierarchy
317
public @interface LessThanUnknown {}
318
```
319

320
**Usage Examples:**
321

322
```java
323
import org.checkerframework.checker.index.qual.*;
324

325
public class ComparisonExample {
326
    // Ensure start is less than end for valid ranges
327
    public void processRange(@LessThan("#2") int start, int end) {
328
        for (int i = start; i < end; i++) {
329
            System.out.println("Processing item: " + i);
330
        }
331
    }
332
    
333
    // Binary search with ordered bounds
334
    public int binarySearch(int[] array, int target, 
335
                           @LessThan("#4") int low, int high) {
336
        while (low < high) {
337
            int mid = (low + high) / 2;
338
            if (array[mid] < target) {
339
                low = mid + 1;
340
            } else {
341
                high = mid;
342
            }
343
        }
344
        return low;
345
    }
346
}
347
```
348

349
### Polymorphic Index Qualifiers
350

351
Polymorphic qualifiers that adapt based on context.
352

353
```java { .api }
354
/**
355
 * Polymorphic index qualifier
356
 */
357
@Documented
358
@Retention(RetentionPolicy.RUNTIME)
359
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
360
@PolymorphicQualifier(LowerBoundUnknown.class)
361
public @interface PolyIndex {}
362

363
/**
364
 * Polymorphic length qualifier
365
 */
366
@Documented
367
@Retention(RetentionPolicy.RUNTIME)
368
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
369
@PolymorphicQualifier(UpperBoundUnknown.class)
370
public @interface PolyLength {}
371

372
/**
373
 * Polymorphic same-length qualifier
374
 */
375
@Documented
376
@Retention(RetentionPolicy.RUNTIME)
377
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
378
@PolymorphicQualifier(SameLenUnknown.class)
379
public @interface PolySameLen {}
380

381
/**
382
 * Polymorphic lower bound qualifier
383
 */
384
@Documented
385
@Retention(RetentionPolicy.RUNTIME)
386
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
387
@PolymorphicQualifier(LowerBoundUnknown.class)
388
public @interface PolyLowerBound {}
389

390
/**
391
 * Polymorphic upper bound qualifier
392
 */
393
@Documented
394
@Retention(RetentionPolicy.RUNTIME)
395
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
396
@PolymorphicQualifier(UpperBoundUnknown.class)
397
public @interface PolyUpperBound {}
398
```
399

400
**Usage Examples:**
401

402
```java
403
import org.checkerframework.checker.index.qual.*;
404

405
public class PolymorphicExample {
406
    // Return type adapts to parameter index properties
407
    public static @PolyIndex int identity(@PolyIndex int value) {
408
        return value;
409
    }
410
    
411
    // Works with different index types
412
    public void example(int[] array) {
413
        @IndexFor("array") int validIndex = 5;
414
        @NonNegative int nonNegValue = 10;
415
        
416
        int result1 = identity(validIndex);  // result1 is @IndexFor("array")
417
        int result2 = identity(nonNegValue); // result2 is @NonNegative
418
    }
419
}
420
```
421

422
### Method Contract Annotations
423

424
Annotations for expressing index-related method contracts.
425

426
```java { .api }
427
/**
428
 * Method postcondition: ensures the specified expression is less than the length of specified arrays
429
 */
430
@Target(ElementType.METHOD)
431
@Retention(RetentionPolicy.RUNTIME)
432
@InheritedAnnotation
433
public @interface EnsuresLTLengthOf {
434
    String[] value();
435
    String[] targetValue();
436
}
437

438
/**
439
 * Conditional method postcondition for length relationships
440
 */
441
@Target(ElementType.METHOD)
442
@Retention(RetentionPolicy.RUNTIME)
443
@InheritedAnnotation
444
public @interface EnsuresLTLengthOfIf {
445
    String[] expression();
446
    boolean result();
447
    String[] targetValue();
448
}
449
```
450

451
**Usage Examples:**
452

453
```java
454
import org.checkerframework.checker.index.qual.*;
455

456
public class ContractExample {
457
    private int currentIndex = 0;
458
    private int[] data = new int[100];
459
    
460
    @EnsuresLTLengthOf(value = "currentIndex", targetValue = "data")
461
    public void reset() {
462
        currentIndex = 0; // Ensures currentIndex < data.length
463
    }
464
    
465
    @EnsuresLTLengthOfIf(expression = "currentIndex", result = true, targetValue = "data")
466
    public boolean hasNext() {
467
        return currentIndex < data.length;
468
    }
469
    
470
    public void safeIteration() {
471
        reset();
472
        while (hasNext()) {
473
            // Safe - postcondition ensures currentIndex < data.length
474
            System.out.println(data[currentIndex]);
475
            currentIndex++;
476
        }
477
    }
478
}
479
```
480

481
### Additional Utility Annotations
482

483
Supporting annotations for complex index relationships.
484

485
```java { .api }
486
/**
487
 * Indicates that one array has a subsequence relationship with another
488
 */
489
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
490
@Retention(RetentionPolicy.RUNTIME)
491
public @interface HasSubsequence {
492
    String[] subsequence();
493
    String[] from();
494
    String[] to();
495
}
496

497
/**
498
 * Indicates a negative index for specified arrays (for reverse indexing)
499
 */
500
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
501
@Retention(RetentionPolicy.RUNTIME)
502
public @interface NegativeIndexFor {
503
    String[] value();
504
}
505

506
/**
507
 * Literal value for upper bound constraints
508
 */
509
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
510
@Retention(RetentionPolicy.RUNTIME)
511
public @interface UpperBoundLiteral {
512
    String[] value();
513
}
514
```
515

516
**Usage Examples:**
517

518
```java
519
import org.checkerframework.checker.index.qual.*;
520

521
public class UtilityExample {
522
    // Subsequence operations
523
    public void copySubsequence(int[] source, int[] dest,
524
                               @HasSubsequence(subsequence = "dest", from = "#3", to = "#4") 
525
                               int[] target,
526
                               int fromIndex, int toIndex) {
527
        System.arraycopy(source, fromIndex, dest, 0, toIndex - fromIndex);
528
    }
529
    
530
    // Reverse indexing (Python-style negative indices)
531
    public int getFromEnd(int[] array, @NegativeIndexFor("#1") int negativeIndex) {
532
        return array[array.length + negativeIndex]; // Safe reverse access
533
    }
534
}
535
```