Optional Checker Annotations

/**
 * The Optional container definitely contains a (non-null) value.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({MaybePresent.class})
public @interface Present {}

import org.checkerframework.checker.optional.qual.Present;
import java.util.Optional;

public class PresentExample {
    // Field is guaranteed to contain a value
    Optional<@Present String> userName;
    
    // Method returns a present Optional
    public Optional<@Present String> getConfigValue() {
        return Optional.of("production"); // Safe - definitely present
    }
    
    // Safe to call .get() on present Optional
    public void processPresent(Optional<@Present String> opt) {
        String value = opt.get(); // Safe - no exception possible
        System.out.println(value.length());
    }
}

/**
 * The Optional container may or may not contain a value.
 * This is the default qualifier in the Optional hierarchy.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf({})
@DefaultQualifierInHierarchy
public @interface MaybePresent {}

import org.checkerframework.checker.optional.qual.MaybePresent;
import java.util.Optional;

public class MaybePresentExample {
    // Default - may be empty
    Optional<String> userInput; // Implicitly @MaybePresent
    
    // Method might return empty Optional
    public Optional<@MaybePresent String> findUser(String id) {
        return userDatabase.findById(id); // Might be empty
    }
    
    // Must check before using .get()
    public void processMaybePresent(Optional<String> opt) {
        if (opt.isPresent()) {
            String value = opt.get(); // Safe after presence check
            System.out.println(value);
        }
        // opt.get(); // ERROR: unsafe without presence check
    }
}

/**
 * A polymorphic qualifier for Optional types.
 * The presence of the return value depends on the presence of the arguments.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(MaybePresent.class)
public @interface PolyPresent {}

import org.checkerframework.checker.optional.qual.PolyPresent;
import java.util.Optional;

public class PolyPresentExample {
    // If input is present, output is present; if input is maybe-present, output is maybe-present
    public Optional<@PolyPresent String> transform(Optional<@PolyPresent String> input) {
        return input.map(String::toUpperCase);
    }
    
    // Type-preserving filtering
    public Optional<@PolyPresent Integer> filterPositive(Optional<@PolyPresent Integer> input) {
        return input.filter(x -> x > 0);
    }
}

/**
 * Indicates that the expression evaluates to a present Optional,
 * if the method terminates successfully.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
@PostconditionAnnotation(qualifier = Present.class)
@InheritedAnnotation
public @interface EnsuresPresent {
    /**
     * The expression (of Optional type) that is present,
     * if the method returns normally.
     */
    String[] value();
}

/**
 * Indicates that the expressions are present if the method
 * returns the specified boolean value.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
@ConditionalPostconditionAnnotation(qualifier = Present.class)
@InheritedAnnotation
public @interface EnsuresPresentIf {
    /** The expressions that are present if the method returns the given result. */
    String[] expression();
    
    /** The return value that indicates the expressions are present. */
    boolean result();
}

import org.checkerframework.checker.optional.qual.*;
import java.util.Optional;

public class PostconditionExample {
    private Optional<String> cachedValue;
    
    // After this method, cachedValue is definitely present
    @EnsuresPresent("cachedValue")
    public void initializeCache() {
        cachedValue = Optional.of("initialized");
    }
    
    // If returns true, the argument is present
    @EnsuresPresentIf(expression = "#1", result = true)
    public boolean validate(Optional<String> input) {
        if (input.isPresent() && input.get().length() > 0) {
            return true; // input is definitely present
        }
        return false;
    }
    
    public void useValidation() {
        Optional<String> opt = getOptionalString();
        if (validate(opt)) {
            // opt is now known to be present
            String value = opt.get(); // Safe
        }
    }
}

/**
 * Indicates a method precondition: the specified expressions of type Optional
 * must be present (non-empty) when the annotated method is invoked.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
@PreconditionAnnotation(qualifier = Present.class)
public @interface RequiresPresent {
    /**
     * The Java expressions that need to be Present.
     */
    String[] value();
    
    @Documented
    @Retention(RetentionPolicy.RUNTIME)
    @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
    @PreconditionAnnotation(qualifier = Present.class)
    public static @interface List {
        RequiresPresent[] value();
    }
}

import org.checkerframework.checker.optional.qual.*;
import java.util.Optional;

public class PreconditionExample {
    private Optional<String> config;
    private Optional<String> backup;
    
    // Requires config to be present before calling
    @RequiresPresent("config")
    public void processConfiguration() {
        String configValue = config.get(); // Safe - precondition ensures presence
        System.out.println("Config: " + configValue);
    }
    
    // Requires multiple Optionals to be present
    @RequiresPresent({"config", "backup"})
    public void synchronizeConfiguration() {
        String primary = config.get();   // Safe
        String secondary = backup.get(); // Safe
        // Synchronization logic...
    }
    
    public void usage() {
        config = Optional.of("production");
        backup = Optional.of("staging");
        
        processConfiguration(); // OK - config is present
        synchronizeConfiguration(); // OK - both are present
        
        config = Optional.empty();
        // processConfiguration(); // ERROR - violates precondition
    }
}

/**
 * Annotation for methods that create Optional instances.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
public @interface OptionalCreator {}

/**
 * Annotation for methods that eliminate/consume Optional instances.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
public @interface OptionalEliminator {}

/**
 * Annotation for methods that propagate Optional presence.
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
public @interface OptionalPropagator {}

// Import statements for using Optional checker annotations
import org.checkerframework.checker.optional.qual.Present;
import org.checkerframework.checker.optional.qual.MaybePresent;
import org.checkerframework.checker.optional.qual.PolyPresent;
import org.checkerframework.checker.optional.qual.EnsuresPresent;
import org.checkerframework.checker.optional.qual.EnsuresPresentIf;
import org.checkerframework.checker.optional.qual.RequiresPresent;
import org.checkerframework.checker.optional.qual.OptionalCreator;
import org.checkerframework.checker.optional.qual.OptionalEliminator;
import org.checkerframework.checker.optional.qual.OptionalPropagator;

// Common patterns for Optional usage
import java.util.Optional;

// Safe Optional usage with annotations
public class OptionalPatterns {
    // Factory method creating present Optional
    @OptionalCreator
    public static Optional<@Present String> ofNonEmpty(String value) {
        if (value.isEmpty()) throw new IllegalArgumentException();
        return Optional.of(value);
    }
    
    // Method safely consuming Optional
    @OptionalEliminator
    public static void ifPresent(Optional<String> opt, Consumer<String> action) {
        if (opt.isPresent()) {
            action.accept(opt.get());
        }
    }
}