tessl/maven-org-checkerframework--checker-qual
Type qualifier annotations for the Checker Framework static analysis tool
—
Pending
index-bounds.mddocs/
Index and Bounds Annotations
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.
Capabilities
Index Validity Annotations
Annotations that specify valid indices for arrays and collections.
/**
* Indicates that the annotated expression is a valid index for the specified arrays
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(LowerBoundUnknown.class)
public @interface IndexFor {
String[] value();
}
/**
* Valid index or the length of specified arrays (useful for insertion operations)
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(UpperBoundUnknown.class)
public @interface IndexOrHigh {
String[] value();
}
/**
* Valid index or -1 for specified arrays (useful for search operations)
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(LowerBoundUnknown.class)
public @interface IndexOrLow {
String[] value();
}Usage Examples:
import org.checkerframework.checker.index.qual.*;
public class IndexExample {
public void processArray(int[] array, @IndexFor("#1") int index) {
System.out.println(array[index]); // Safe - index is valid for array
}
public void insertAt(int[] array, @IndexOrHigh("#1") int position, int value) {
// Can insert at any valid index or at the end (position == array.length)
if (position < array.length) {
array[position] = value; // Safe insertion
}
}
public @IndexOrLow("#1") int find(int[] array, int target) {
for (int i = 0; i < array.length; i++) {
if (array[i] == target) {
return i; // Returns valid index
}
}
return -1; // Returns -1 if not found
}
}Numeric Range Annotations
Annotations for specifying numeric ranges and constraints.
/**
* Indicates that the annotated expression evaluates to an integer >= 0
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(GTENegativeOne.class)
public @interface NonNegative {}
/**
* Indicates that the annotated expression evaluates to an integer > 0
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(NonNegative.class)
public @interface Positive {}
/**
* Indicates that the annotated expression evaluates to an integer >= -1
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(LowerBoundUnknown.class)
public @interface GTENegativeOne {}Usage Examples:
import org.checkerframework.checker.index.qual.*;
public class RangeExample {
// Array size must be non-negative
public int[] createArray(@NonNegative int size) {
return new int[size]; // Safe - size >= 0
}
// Count must be positive for meaningful operations
public void repeat(@Positive int count, Runnable action) {
for (int i = 0; i < count; i++) {
action.run();
}
}
// Search result: valid index or -1
public @GTENegativeOne int binarySearch(int[] array, int target) {
// Implementation returns valid index or -1
return java.util.Arrays.binarySearch(array, target);
}
}Length Relationship Annotations
Annotations that express relationships between array lengths and indices.
/**
* Indicates arrays have the same length
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(SameLenUnknown.class)
public @interface SameLen {
String[] value();
}
/**
* Expression is the length of specified arrays
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(UpperBoundUnknown.class)
public @interface LengthOf {
String[] value();
}
/**
* Expression is less than the length of specified arrays
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(LTEqLengthOf.class)
public @interface LTLengthOf {
String[] value();
}
/**
* Expression is less than or equal to the length of specified arrays
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(UpperBoundUnknown.class)
public @interface LTEqLengthOf {
String[] value();
}
/**
* Expression is less than the length minus one of specified arrays
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(LTLengthOf.class)
public @interface LTOMLengthOf {
String[] value();
}Usage Examples:
import org.checkerframework.checker.index.qual.*;
public class LengthExample {
// Process arrays of same length
public void processParallel(@SameLen("#2") int[] array1, int[] array2) {
for (int i = 0; i < array1.length; i++) {
// Safe - arrays have same length
System.out.println(array1[i] + array2[i]);
}
}
// Size parameter represents array length
public void processWithSize(int[] array, @LengthOf("#1") int size) {
for (int i = 0; i < size; i++) {
System.out.println(array[i]); // Safe - i < size == array.length
}
}
// Index is less than array length
public void safeAccess(int[] array, @LTLengthOf("#1") int index) {
System.out.println(array[index]); // Safe - index < array.length
}
}Search and Substring Operations
Specialized annotations for search operations and string manipulation.
/**
* Result of a search operation: valid index or -1
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(SearchIndexUnknown.class)
public @interface SearchIndexFor {
String[] value();
}
/**
* Result of substring operations
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(SubstringIndexUnknown.class)
public @interface SubstringIndexFor {
String[] value();
}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(SearchIndexFor.class)
public @interface SearchIndexBottom {}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@DefaultQualifierInHierarchy
public @interface SearchIndexUnknown {}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(SubstringIndexFor.class)
public @interface SubstringIndexBottom {}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@DefaultQualifierInHierarchy
public @interface SubstringIndexUnknown {}Usage Examples:
import org.checkerframework.checker.index.qual.*;
public class SearchExample {
public @SearchIndexFor("#1") int findValue(int[] array, int target) {
for (int i = 0; i < array.length; i++) {
if (array[i] == target) {
return i;
}
}
return -1;
}
public @SubstringIndexFor("#1") int findSubstring(String text, String pattern) {
return text.indexOf(pattern); // Returns valid index or -1
}
public void useSearchResult(String text, String pattern) {
@SubstringIndexFor("text") int index = findSubstring(text, pattern);
if (index >= 0) {
// Safe to use index for substring operations
String found = text.substring(index, index + pattern.length());
System.out.println("Found: " + found);
}
}
}Comparison and Ordering Annotations
Annotations for expressing ordering relationships between expressions.
/**
* Expression is less than the specified expressions
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(LessThanUnknown.class)
public @interface LessThan {
String[] value();
}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(LessThan.class)
public @interface LessThanBottom {}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@DefaultQualifierInHierarchy
public @interface LessThanUnknown {}Usage Examples:
import org.checkerframework.checker.index.qual.*;
public class ComparisonExample {
// Ensure start is less than end for valid ranges
public void processRange(@LessThan("#2") int start, int end) {
for (int i = start; i < end; i++) {
System.out.println("Processing item: " + i);
}
}
// Binary search with ordered bounds
public int binarySearch(int[] array, int target,
@LessThan("#4") int low, int high) {
while (low < high) {
int mid = (low + high) / 2;
if (array[mid] < target) {
low = mid + 1;
} else {
high = mid;
}
}
return low;
}
}Polymorphic Index Qualifiers
Polymorphic qualifiers that adapt based on context.
/**
* Polymorphic index qualifier
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(LowerBoundUnknown.class)
public @interface PolyIndex {}
/**
* Polymorphic length qualifier
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(UpperBoundUnknown.class)
public @interface PolyLength {}
/**
* Polymorphic same-length qualifier
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(SameLenUnknown.class)
public @interface PolySameLen {}
/**
* Polymorphic lower bound qualifier
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(LowerBoundUnknown.class)
public @interface PolyLowerBound {}
/**
* Polymorphic upper bound qualifier
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(UpperBoundUnknown.class)
public @interface PolyUpperBound {}Usage Examples:
import org.checkerframework.checker.index.qual.*;
public class PolymorphicExample {
// Return type adapts to parameter index properties
public static @PolyIndex int identity(@PolyIndex int value) {
return value;
}
// Works with different index types
public void example(int[] array) {
@IndexFor("array") int validIndex = 5;
@NonNegative int nonNegValue = 10;
int result1 = identity(validIndex); // result1 is @IndexFor("array")
int result2 = identity(nonNegValue); // result2 is @NonNegative
}
}Method Contract Annotations
Annotations for expressing index-related method contracts.
/**
* Method postcondition: ensures the specified expression is less than the length of specified arrays
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresLTLengthOf {
String[] value();
String[] targetValue();
}
/**
* Conditional method postcondition for length relationships
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresLTLengthOfIf {
String[] expression();
boolean result();
String[] targetValue();
}Usage Examples:
import org.checkerframework.checker.index.qual.*;
public class ContractExample {
private int currentIndex = 0;
private int[] data = new int[100];
@EnsuresLTLengthOf(value = "currentIndex", targetValue = "data")
public void reset() {
currentIndex = 0; // Ensures currentIndex < data.length
}
@EnsuresLTLengthOfIf(expression = "currentIndex", result = true, targetValue = "data")
public boolean hasNext() {
return currentIndex < data.length;
}
public void safeIteration() {
reset();
while (hasNext()) {
// Safe - postcondition ensures currentIndex < data.length
System.out.println(data[currentIndex]);
currentIndex++;
}
}
}Additional Utility Annotations
Supporting annotations for complex index relationships.
/**
* Indicates that one array has a subsequence relationship with another
*/
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
public @interface HasSubsequence {
String[] subsequence();
String[] from();
String[] to();
}
/**
* Indicates a negative index for specified arrays (for reverse indexing)
*/
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
public @interface NegativeIndexFor {
String[] value();
}
/**
* Literal value for upper bound constraints
*/
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@Retention(RetentionPolicy.RUNTIME)
public @interface UpperBoundLiteral {
String[] value();
}Usage Examples:
import org.checkerframework.checker.index.qual.*;
public class UtilityExample {
// Subsequence operations
public void copySubsequence(int[] source, int[] dest,
@HasSubsequence(subsequence = "dest", from = "#3", to = "#4")
int[] target,
int fromIndex, int toIndex) {
System.arraycopy(source, fromIndex, dest, 0, toIndex - fromIndex);
}
// Reverse indexing (Python-style negative indices)
public int getFromEnd(int[] array, @NegativeIndexFor("#1") int negativeIndex) {
return array[array.length + negativeIndex]; // Safe reverse access
}
}Install with Tessl CLI
npx tessl i tessl/maven-org-checkerframework--checker-qual