Resource Management Annotations

/**
 * Specifies methods that must be called on this object
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(MustCallUnknown.class)
public @interface MustCall {
    String[] value();
}

/**
 * Creates an alias for must-call obligations
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER, ElementType.PARAMETER})
@SubtypeOf(MustCall.class)
public @interface MustCallAlias {}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@DefaultQualifierInHierarchy
public @interface MustCallUnknown {}

/**
 * Polymorphic must-call qualifier
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@PolymorphicQualifier(MustCallUnknown.class)
public @interface PolyMustCall {}

/**
 * Inheritable must-call annotation for class hierarchies
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.TYPE)
@InheritedAnnotation
public @interface InheritableMustCall {
    String[] value();
}

import org.checkerframework.checker.mustcall.qual.*;
import java.io.*;

// File must have close() called
@InheritableMustCall("close")
public class ManagedFile {
    private FileInputStream stream;
    
    public ManagedFile(String filename) throws IOException {
        this.stream = new FileInputStream(filename);
    }
    
    public int read() throws IOException {
        return stream.read();
    }
    
    public void close() throws IOException {
        if (stream != null) {
            stream.close();
            stream = null;
        }
    }
}

public class ResourceExample {
    public void processFile(String filename) throws IOException {
        @MustCall("close") ManagedFile file = new ManagedFile(filename);
        try {
            int data = file.read();
            System.out.println("Read: " + data);
        } finally {
            file.close(); // Required - must call close()
        }
    }
    
    // Polymorphic method preserves must-call obligations
    public @PolyMustCall ManagedFile processResource(@PolyMustCall ManagedFile resource) {
        // Process the resource without changing its must-call obligation
        return resource;
    }
    
    // Try-with-resources automatically handles must-call
    public void safeProcessing(String filename) throws IOException {
        try (@MustCall("close") ManagedFile file = new ManagedFile(filename)) {
            int data = file.read();
            System.out.println("Read: " + data);
        } // close() called automatically
    }
}

/**
 * Indicates which methods have been called on the object
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(CalledMethodsBottom.class)
public @interface CalledMethods {
    String[] value();
}

@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
@SubtypeOf(CalledMethods.class)
public @interface CalledMethodsBottom {}

/**
 * Predicate over called methods (for complex conditions)
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
public @interface CalledMethodsPredicate {
    String value();
}

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

public class DatabaseConnection {
    private boolean connected = false;
    private boolean authenticated = false;
    
    public void connect() {
        this.connected = true;
    }
    
    public void authenticate(String username, String password) {
        if (!connected) {
            throw new IllegalStateException("Must connect first");
        }
        this.authenticated = true;
    }
    
    public void executeQuery(String query) {
        if (!connected || !authenticated) {
            throw new IllegalStateException("Must connect and authenticate first");
        }
        System.out.println("Executing: " + query);
    }
    
    public void disconnect() {
        this.connected = false;
        this.authenticated = false;
    }
}

public class CalledMethodsExample {
    public void safeDatabase() {
        DatabaseConnection db = new DatabaseConnection();
        
        // Track method calls
        db.connect();
        @CalledMethods("connect") DatabaseConnection connectedDb = db;
        
        db.authenticate("user", "pass");
        @CalledMethods({"connect", "authenticate"}) DatabaseConnection authDb = db;
        
        // Safe to execute query after both methods called
        authDb.executeQuery("SELECT * FROM users");
        
        db.disconnect();
    }
    
    // Method that requires specific methods to have been called
    public void processConnectedDatabase(@CalledMethods("connect") DatabaseConnection db) {
        // Can safely assume connect() has been called
        db.authenticate("admin", "secret");
        db.executeQuery("SELECT * FROM admin_table");
    }
}

/**
 * Parameter takes ownership of the resource
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.PARAMETER)
public @interface Owning {}

/**
 * Parameter does not take ownership of the resource
 */
@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.PARAMETER)
public @interface NotOwning {}

import org.checkerframework.checker.mustcall.qual.*;
import java.io.Closeable;

public class OwnershipExample {
    // Method takes ownership and is responsible for closing
    public void processAndClose(@Owning @MustCall("close") Closeable resource) {
        try {
            // Process the resource
            System.out.println("Processing resource");
        } finally {
            try {
                resource.close(); // Owner must close
            } catch (Exception e) {
                // Handle close error
            }
        }
    }
    
    // Method uses resource but doesn't take ownership
    public void processOnly(@NotOwning @MustCall("close") Closeable resource) {
        // Use the resource but don't close it
        System.out.println("Using resource");
        // Caller is still responsible for closing
    }
    
    public void example() throws Exception {
        @MustCall("close") FileInputStream file = new FileInputStream("data.txt");
        
        // Transfer ownership - file will be closed by processAndClose
        processAndClose(file);
        // Don't close file here - ownership was transferred
        
        @MustCall("close") FileInputStream file2 = new FileInputStream("data2.txt");
        try {
            // Use without transferring ownership
            processOnly(file2);
            // Still responsible for closing since ownership not transferred
        } finally {
            file2.close();
        }
    }
}

/**
 * Method creates must-call obligations for specified expressions
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface CreatesMustCallFor {
    String[] value();
}

import org.checkerframework.checker.mustcall.qual.*;
import java.io.*;

public class ConnectionPool {
    private List<@MustCall("close") Connection> activeConnections = new ArrayList<>();
    
    @CreatesMustCallFor("this")
    public Connection borrowConnection() {
        @MustCall("close") Connection conn = new Connection();
        activeConnections.add(conn);
        return conn; // Creates must-call obligation for the pool
    }
    
    public void returnConnection(@MustCall("close") Connection conn) {
        activeConnections.remove(conn);
        // Connection is returned to pool, not closed yet
    }
    
    @MustCall("closeAll")
    public void closeAll() {
        for (@MustCall("close") Connection conn : activeConnections) {
            try {
                conn.close();
            } catch (Exception e) {
                // Log error
            }
        }
        activeConnections.clear();
    }
}

@MustCall("close")
class Connection {
    private boolean closed = false;
    
    public void execute(String command) {
        if (closed) throw new IllegalStateException("Connection closed");
        System.out.println("Executing: " + command);
    }
    
    public void close() {
        this.closed = true;
    }
}

public class SideEffectExample {
    public void useConnectionPool() {
        @MustCall("closeAll") ConnectionPool pool = new ConnectionPool();
        
        // borrowConnection creates must-call obligation for pool
        @MustCall("close") Connection conn1 = pool.borrowConnection();
        @MustCall("close") Connection conn2 = pool.borrowConnection();
        
        try {
            conn1.execute("SELECT * FROM users");
            conn2.execute("UPDATE settings SET value = 'new' WHERE key = 'config'");
        } finally {
            // Return connections to pool
            pool.returnConnection(conn1);
            pool.returnConnection(conn2);
            
            // Pool must close all connections
            pool.closeAll(); // Required due to @CreatesMustCallFor
        }
    }
}

/**
 * Method postcondition: ensures specified methods are called on expressions
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresCalledMethods {
    String[] value();
    String[] methods();
}

/**
 * Conditional method postcondition for called methods
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresCalledMethodsIf {
    String[] expression();
    String[] methods();
    boolean result();
}

/**
 * Exception postcondition: ensures methods are called when exception thrown
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresCalledMethodsOnException {
    String[] value();
    String[] methods();
    Class<? extends Throwable>[] exception() default {Throwable.class};
}

/**
 * Varargs version of EnsuresCalledMethods
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface EnsuresCalledMethodsVarargs {
    String[] value();
    String[] methods();
}

/**
 * Method precondition: requires specified methods to have been called
 */
@Target(ElementType.METHOD)
@Retention(RetentionPolicy.RUNTIME)
@InheritedAnnotation
public @interface RequiresCalledMethods {
    String[] value();
    String[] methods();
}

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

public class ContractResourceExample {
    private DatabaseConnection connection;
    
    @EnsuresCalledMethods(value = "connection", methods = {"connect"})
    public void initialize() {
        connection = new DatabaseConnection();
        connection.connect(); // Postcondition ensures connect() is called
    }
    
    @EnsuresCalledMethodsIf(expression = "connection", methods = {"connect", "authenticate"}, result = true)
    public boolean isReady() {
        return connection != null && 
               connection.isConnected() && 
               connection.isAuthenticated();
    }
    
    @RequiresCalledMethods(value = "connection", methods = {"connect"})
    public void authenticate(String user, String password) {
        // Precondition: connect() must have been called
        connection.authenticate(user, password);
    }
    
    @EnsuresCalledMethodsOnException(value = "connection", methods = {"disconnect"}, exception = {SQLException.class})
    public void riskyOperation() throws SQLException {
        try {
            connection.executeQuery("RISKY OPERATION");
        } catch (SQLException e) {
            connection.disconnect(); // Cleanup on exception
            throw e;
        }
    }
    
    public void safeUsage() throws SQLException {
        initialize(); // Ensures connect() is called
        authenticate("user", "pass"); // Safe - connect() was called
        
        if (isReady()) {
            // Safe - conditional postcondition ensures both methods called
            connection.executeQuery("SELECT * FROM data");
        }
        
        try {
            riskyOperation();
        } catch (SQLException e) {
            // Exception postcondition ensures disconnect() was called
            System.out.println("Operation failed, connection cleaned up");
        }
    }
}