CtrlK
BlogDocsLog inGet started
Tessl Logo

tessl/maven-org-checkerframework--checker-qual

Type qualifier annotations for the Checker Framework static analysis tool

—

Pending
Overview
Eval results
Files

contracts.mddocs/

Method Contracts and Side Effects

Method contract annotations specify method behavior, purity, and side effects. These annotations help verify that methods behave as expected and maintain system invariants.

Capabilities

Purity Annotations

Annotations that specify method purity and side effect properties.

/**
 * Method has no side effects and returns the same result for same inputs
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface Pure {}

/**
 * Method has no side effects but may return different results (e.g., getCurrentTime)
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface SideEffectFree {}

/**
 * Method returns the same result for same inputs but may have side effects
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface Deterministic {}

/**
 * Method terminates execution (throws exception or calls System.exit)
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface TerminatesExecution {}

/**
 * Indicates method is unqualified for purity analysis
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.METHOD)
public @interface PurityUnqualified {}

Usage Examples:

import org.checkerframework.dataflow.qual.*;

public class PurityExample {
    private int counter = 0;
    
    // Pure method - no side effects, same result for same inputs
    @Pure
    public int add(int a, int b) {
        return a + b; // Always returns same result for same inputs
    }
    
    // Side-effect free but not deterministic
    @SideEffectFree
    public long getCurrentTime() {
        return System.currentTimeMillis(); // No side effects, but result varies
    }
    
    // Deterministic but has side effects
    @Deterministic
    public int getAndIncrement() {
        return counter++; // Side effect: modifies counter, but deterministic sequence
    }
    
    // Method that always throws exception
    @TerminatesExecution
    public void fail(String message) {
        throw new RuntimeException(message); // Never returns normally
    }
    
    // Complex method that can't be classified for purity
    @PurityUnqualified
    public void complexOperation() {
        // Complex logic that doesn't fit purity categories
        if (Math.random() > 0.5) {
            counter++;
        }
        System.out.println("Operation complete");
    }
    
    public void example() {
        // Pure methods can be called multiple times safely
        int result1 = add(5, 3); // 8
        int result2 = add(5, 3); // Always 8
        assert result1 == result2; // Always true
        
        // Side-effect free methods don't modify state
        long time1 = getCurrentTime();
        long time2 = getCurrentTime(); // May be different
        
        // Deterministic methods have predictable sequences
        int seq1 = getAndIncrement(); // 0
        int seq2 = getAndIncrement(); // 1
        int seq3 = getAndIncrement(); // 2
        
        // Method that terminates execution
        try {
            fail("Something went wrong");
        } catch (RuntimeException e) {
            System.out.println("Caught expected exception");
        }
    }
}

Nullness Contract Annotations

Method contracts specifically for nullness properties (covered in detail in nullness.md).

/**
 * Method postcondition: ensures expressions are non-null after execution
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresNonNull {
    String[] value();
}

/**
 * Conditional nullness postcondition
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresNonNullIf {
    String[] expression();
    boolean result();
}

/**
 * Method precondition: requires expressions to be non-null
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface RequiresNonNull {
    String[] value();
}

Usage Examples:

import org.checkerframework.checker.nullness.qual.*;

public class NullnessContractExample {
    private String data;
    private String backup;
    
    @EnsuresNonNull("data")
    public void initializeData(String value) {
        this.data = value; // Postcondition: data is non-null
    }
    
    @EnsuresNonNullIf(expression = {"data", "backup"}, result = true)
    public boolean isFullyInitialized() {
        return data != null && backup != null;
    }
    
    @RequiresNonNull("data")
    public void processData() {
        // Precondition: data must be non-null
        System.out.println("Processing: " + data.length() + " characters");
    }
    
    @EnsuresNonNull("backup")
    public void createBackup() {
        this.backup = this.data != null ? this.data + "_backup" : "empty_backup";
    }
    
    public void safeWorkflow() {
        initializeData("Hello World"); // Ensures data is non-null
        processData(); // Safe - postcondition guarantees data is non-null
        
        createBackup(); // Ensures backup is non-null
        
        if (isFullyInitialized()) {
            // Safe - conditional postcondition guarantees both are non-null
            System.out.println("Data: " + data + ", Backup: " + backup);
        }
    }
}

Lock Contract Annotations

Method contracts for concurrency and locking (covered in detail in concurrency.md).

/**
 * Method requires specified locks to be held when called
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface Holding {
    String[] value();
}

/**
 * Method postcondition: ensures locks are held after execution
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresLockHeld {
    String[] value();
}

/**
 * Conditional lock postcondition
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresLockHeldIf {
    String[] expression();
    boolean result();
}

Usage Examples:

import org.checkerframework.checker.lock.qual.*;

public class LockContractExample {
    private final Object dataLock = new Object();
    private final Object stateLock = new Object();
    private String sharedData;
    private boolean initialized = false;
    
    @EnsuresLockHeld("dataLock")
    public void acquireDataLock() {
        synchronized (dataLock) {
            // Lock acquired - postcondition ensures it's held
        }
    }
    
    @Holding("dataLock")
    public void updateData(String newData) {
        // Precondition: dataLock must be held
        this.sharedData = newData;
    }
    
    @EnsuresLockHeldIf(expression = "stateLock", result = true)
    public boolean tryInitialize() {
        synchronized (stateLock) {
            if (!initialized) {
                initialized = true;
                return true; // Lock is held when returning true
            }
        }
        return false; // Lock not held when returning false
    }
    
    public void concurrentWorkflow() {
        synchronized (dataLock) {
            updateData("New value"); // Safe - lock is held
        }
        
        if (tryInitialize()) {
            // Safe - conditional postcondition ensures stateLock is held
            // Can safely access state protected by stateLock
            System.out.println("Initialization successful");
        }
    }
}

Index and Bounds Contract Annotations

Method contracts for array bounds and index relationships (covered in detail in index-bounds.md).

/**
 * Method postcondition: ensures expression is less than length of arrays
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresLTLengthOf {
    String[] value();
    String[] targetValue();
}

/**
 * Conditional bounds postcondition
 */
@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 BoundsContractExample {
    private int[] data = new int[100];
    private int currentIndex = 0;
    
    @EnsuresLTLengthOf(value = "currentIndex", targetValue = "data")
    public void resetIndex() {
        currentIndex = 0; // Postcondition: currentIndex < data.length
    }
    
    @EnsuresLTLengthOfIf(expression = "currentIndex", result = true, targetValue = "data")
    public boolean hasNext() {
        return currentIndex < data.length;
    }
    
    public void safeBoundsIteration() {
        resetIndex(); // Ensures currentIndex < data.length
        
        while (hasNext()) {
            // Safe - conditional postcondition ensures currentIndex < data.length
            System.out.println(data[currentIndex]);
            currentIndex++;
        }
    }
}

Generic Contract Framework

Framework for creating custom method contracts.

/**
 * Generic method postcondition
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresQualifier {
    String[] expression();
    Class<? extends Annotation> qualifier();
}

/**
 * Generic conditional method postcondition
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresQualifierIf {
    String[] expression();
    Class<? extends Annotation> qualifier();
    boolean result();
}

/**
 * Generic method precondition
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface RequiresQualifier {
    String[] expression();
    Class<? extends Annotation> qualifier();
}

Usage Examples:

import org.checkerframework.framework.qual.*;

// Custom qualifier for validated input
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface Validated {}

// Custom qualifier for sanitized data
@Target({ElementType.TYPE_USE})
@Retention(RetentionPolicy.RUNTIME)
public @interface Sanitized {}

public class GenericContractExample {
    @EnsuresQualifier(expression = "#1", qualifier = Validated.class)
    public String validate(String input) {
        if (input == null || input.trim().isEmpty()) {
            throw new IllegalArgumentException("Invalid input");
        }
        return input; // Postcondition: result is @Validated
    }
    
    @RequiresQualifier(expression = "#1", qualifier = Validated.class)
    @EnsuresQualifier(expression = "#1", qualifier = Sanitized.class)
    public String sanitize(@Validated String input) {
        // Precondition: input must be @Validated
        // Remove potentially dangerous characters
        String sanitized = input.replaceAll("[<>\"'&]", "");
        return sanitized; // Postcondition: result is @Sanitized
    }
    
    @EnsuresQualifierIf(expression = "#1", qualifier = Validated.class, result = true)
    public boolean isValid(String input) {
        return input != null && !input.trim().isEmpty();
    }
    
    public void processingPipeline(String userInput) {
        if (isValid(userInput)) {
            // Conditional postcondition: userInput is @Validated
            @Validated String validInput = (@Validated String) userInput;
            
            @Sanitized String safeInput = sanitize(validInput); // Safe - precondition met
            
            // Use sanitized input safely
            System.out.println("Processing: " + safeInput);
        } else {
            System.out.println("Invalid input provided");
        }
    }
}

Advanced Contract Patterns

Complex contract combinations and patterns.

Builder Pattern with Contracts:

import org.checkerframework.checker.calledmethods.qual.*;
import org.checkerframework.dataflow.qual.*;

public class ContractBuilderExample {
    @MustCall("build")
    public static class ConfigBuilder {
        private String host;
        private int port = 80;
        private boolean secure = false;
        
        @EnsuresCalledMethods(value = "this", methods = {"setHost"})
        public ConfigBuilder host(String host) {
            this.host = host;
            return this;
        }
        
        public ConfigBuilder port(int port) {
            this.port = port;
            return this;
        }
        
        public ConfigBuilder secure(boolean secure) {
            this.secure = secure;
            return this;
        }
        
        @RequiresCalledMethods(value = "this", methods = {"setHost"})
        @Pure
        public Config build() {
            return new Config(host, port, secure);
        }
    }
    
    public static class Config {
        private final String host;
        private final int port;
        private final boolean secure;
        
        Config(String host, int port, boolean secure) {
            this.host = host;
            this.port = port;
            this.secure = secure;
        }
        
        @Pure
        public String getHost() { return host; }
        
        @Pure
        public int getPort() { return port; }
        
        @Pure
        public boolean isSecure() { return secure; }
    }
    
    public void builderExample() {
        // Correct usage - host is required
        Config config1 = new ConfigBuilder()
            .host("example.com")  // Required method call
            .port(443)
            .secure(true)
            .build(); // Safe - host was called
        
        // This would cause a type error:
        // Config config2 = new ConfigBuilder()
        //     .port(80)
        //     .build(); // Error - host() must be called first
    }
}

Install with Tessl CLI

npx tessl i tessl/maven-org-checkerframework--checker-qual

docs

concurrency.md

constant-value.md

contracts.md

framework.md

index-bounds.md

index.md

nullness.md

optional.md

resources.md

signedness.md

string-format.md

units.md

tile.json