tessl/maven-org-checkerframework--checker-qual
Type qualifier annotations for the Checker Framework static analysis tool
—
Pending
nullness.mddocs/
Nullness Annotations
Nullness checking annotations prevent null pointer exceptions through static analysis. These annotations specify whether expressions can evaluate to null, enabling the Checker Framework to verify null-safety at compile time.
Capabilities
NonNull Annotation
Indicates that an expression never evaluates to null. This is typically the default annotation and rarely needs to be written explicitly.
/**
* Indicates that the annotated expression never evaluates to null
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(MonotonicNonNull.class)
@DefaultQualifierInHierarchy
public @interface NonNull {}Usage Examples:
import org.checkerframework.checker.nullness.qual.NonNull;
public class NonNullExample {
// Method parameter is never null
public void process(@NonNull String input) {
System.out.println(input.length()); // Safe - no null check needed
}
// Return value is never null
public @NonNull String getName() {
return "default"; // Must return non-null value
}
}Nullable Annotation
Indicates that an expression may evaluate to null. This makes the type include the null value.
/**
* Indicates that the annotated expression may evaluate to null
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({})
@QualifierForLiterals(LiteralKind.NULL)
@DefaultFor(types = Void.class)
public @interface Nullable {}Usage Examples:
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.NonNull;
public class NullableExample {
// Parameter may be null
public void process(@Nullable String input) {
if (input != null) {
System.out.println(input.length()); // Null check required
}
}
// Return value may be null
public @Nullable String findUser(int id) {
return id > 0 ? "user" + id : null;
}
// Convert nullable to non-null
public @NonNull String getDisplayName(@Nullable String name) {
return name != null ? name : "Anonymous";
}
}MonotonicNonNull Annotation
Indicates that a reference starts out null, but once it becomes non-null, it never becomes null again. Commonly used for lazy initialization.
/**
* Indicates that a reference starts null, becomes non-null, and stays non-null
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(Nullable.class)
public @interface MonotonicNonNull {}Usage Examples:
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
public class MonotonicExample {
private @MonotonicNonNull String cachedValue;
@EnsuresNonNull("cachedValue")
public void initialize() {
if (cachedValue == null) {
cachedValue = computeExpensiveValue();
}
}
public String getValue() {
if (cachedValue == null) {
initialize();
}
return cachedValue; // Safe after initialization
}
private String computeExpensiveValue() {
return "computed value";
}
}PolyNull Annotation
Polymorphic qualifier that adapts based on the nullness of other expressions in the same method. If any argument is nullable, the result is nullable; if all arguments are non-null, the result is non-null.
/**
* Polymorphic nullness qualifier that adapts based on context
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(Nullable.class)
public @interface PolyNull {}Usage Examples:
import org.checkerframework.checker.nullness.qual.PolyNull;
public class PolyNullExample {
// Return type adapts to parameter nullness
public static @PolyNull String identity(@PolyNull String input) {
return input;
}
public void example() {
String nonNull = "hello";
String nullable = Math.random() > 0.5 ? "world" : null;
String result1 = identity(nonNull); // result1 is @NonNull
String result2 = identity(nullable); // result2 is @Nullable
}
}KeyFor Annotations
Annotations for tracking map key relationships, ensuring that values are valid keys for specified maps.
/**
* Indicates that the annotated expression is a key for the specified maps
*/
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(UnknownKeyFor.class)
public @interface KeyFor {
String[] value();
}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@ImplicitFor(literals = LiteralKind.NULL)
@SubtypeOf(KeyFor.class)
public @interface KeyForBottom {}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({})
@DefaultQualifierInHierarchy
public @interface UnknownKeyFor {}
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(UnknownKeyFor.class)
public @interface PolyKeyFor {}Usage Examples:
import org.checkerframework.checker.nullness.qual.KeyFor;
import java.util.Map;
public class KeyForExample {
private Map<String, Integer> scores = new HashMap<>();
private Map<String, String> names = new HashMap<>();
public void addScore(String player, int score) {
scores.put(player, score);
names.put(player, player.toUpperCase());
}
// Parameter must be a key in the scores map
public int getScore(@KeyFor("scores") String player) {
return scores.get(player); // Safe - no null check needed
}
// Parameter must be a key in both maps
public void updatePlayer(@KeyFor({"scores", "names"}) String player, int newScore) {
scores.put(player, newScore);
System.out.println("Updated " + names.get(player));
}
}Method Contract Annotations
Annotations for expressing nullness-related method contracts as preconditions and postconditions.
/**
* Method postcondition: ensures the specified expressions are non-null after method execution
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresNonNull {
String[] value();
}
/**
* Conditional method postcondition: ensures expressions are non-null if method returns specified result
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresNonNullIf {
String[] expression();
boolean result();
}
/**
* Method precondition: requires the specified expressions to be non-null when method is called
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface RequiresNonNull {
String[] value();
}
/**
* Ensures key relationships for map operations
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresKeyFor {
String[] expression();
String[] map();
}
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresKeyForIf {
String[] expression();
boolean result();
String[] map();
}Usage Examples:
import org.checkerframework.checker.nullness.qual.*;
public class ContractExample {
private String name;
private String email;
@EnsuresNonNull({"name", "email"})
public void initialize(String n, String e) {
this.name = n;
this.email = e;
}
@EnsuresNonNullIf(expression = "name", result = true)
public boolean isInitialized() {
return name != null && email != null;
}
@RequiresNonNull({"name", "email"})
public void sendWelcomeEmail() {
System.out.println("Sending email to " + name + " at " + email);
}
public void safeUsage() {
initialize("John", "john@example.com");
sendWelcomeEmail(); // Safe - postcondition ensures non-null
if (isInitialized()) {
System.out.println("User: " + name); // Safe - conditional postcondition
}
}
}Utility Annotations
Additional nullness-related utility annotations for special cases.
/**
* Assertion propagation: if parameter becomes non-null, ensure the return value is also non-null
*/
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface AssertNonNullIfNonNull {
String[] value();
}Usage Examples:
import org.checkerframework.checker.nullness.qual.AssertNonNullIfNonNull;
public class UtilityExample {
@AssertNonNullIfNonNull("input")
public static String processString(@Nullable String input) {
return input == null ? null : input.trim();
}
public void example() {
String result1 = processString(null); // result1 is @Nullable
String result2 = processString("hello"); // result2 is @NonNull
}
}Install with Tessl CLI
npx tessl i tessl/maven-org-checkerframework--checker-qual