0
# Resource Management Annotations
1

2
Resource management annotations track object lifecycle and ensure proper cleanup of resources. These annotations help prevent resource leaks by tracking which methods must be called and which objects own resources.
3

4
## Capabilities
5

6
### Must-Call Annotations
7

8
Annotations that specify which methods must be called on objects before they are deallocated.
9

10
```java { .api }
11
/**
12
 * Specifies methods that must be called on this object
13
 */
14
@Documented
15
@Retention(RetentionPolicy.RUNTIME)
16
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
17
@SubtypeOf(MustCallUnknown.class)
18
public @interface MustCall {
19
    String[] value();
20
}
21

22
/**
23
 * Creates an alias for must-call obligations
24
 */
25
@Documented
26
@Retention(RetentionPolicy.RUNTIME)
27
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER, ElementType.PARAMETER})
28
@SubtypeOf(MustCall.class)
29
public @interface MustCallAlias {}
30

31
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
32
@DefaultQualifierInHierarchy
33
public @interface MustCallUnknown {}
34

35
/**
36
 * Polymorphic must-call qualifier
37
 */
38
@Documented
39
@Retention(RetentionPolicy.RUNTIME)
40
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
41
@PolymorphicQualifier(MustCallUnknown.class)
42
public @interface PolyMustCall {}
43

44
/**
45
 * Inheritable must-call annotation for class hierarchies
46
 */
47
@Documented
48
@Retention(RetentionPolicy.RUNTIME)
49
@Target(ElementType.TYPE)
50
@InheritedAnnotation
51
public @interface InheritableMustCall {
52
    String[] value();
53
}
54
```
55

56
**Usage Examples:**
57

58
```java
59
import org.checkerframework.checker.mustcall.qual.*;
60
import java.io.*;
61

62
// File must have close() called
63
@InheritableMustCall("close")
64
public class ManagedFile {
65
    private FileInputStream stream;
66
    
67
    public ManagedFile(String filename) throws IOException {
68
        this.stream = new FileInputStream(filename);
69
    }
70
    
71
    public int read() throws IOException {
72
        return stream.read();
73
    }
74
    
75
    public void close() throws IOException {
76
        if (stream != null) {
77
            stream.close();
78
            stream = null;
79
        }
80
    }
81
}
82

83
public class ResourceExample {
84
    public void processFile(String filename) throws IOException {
85
        @MustCall("close") ManagedFile file = new ManagedFile(filename);
86
        try {
87
            int data = file.read();
88
            System.out.println("Read: " + data);
89
        } finally {
90
            file.close(); // Required - must call close()
91
        }
92
    }
93
    
94
    // Polymorphic method preserves must-call obligations
95
    public @PolyMustCall ManagedFile processResource(@PolyMustCall ManagedFile resource) {
96
        // Process the resource without changing its must-call obligation
97
        return resource;
98
    }
99
    
100
    // Try-with-resources automatically handles must-call
101
    public void safeProcessing(String filename) throws IOException {
102
        try (@MustCall("close") ManagedFile file = new ManagedFile(filename)) {
103
            int data = file.read();
104
            System.out.println("Read: " + data);
105
        } // close() called automatically
106
    }
107
}
108
```
109

110
### Called Methods Tracking
111

112
Annotations that track which methods have been called on objects.
113

114
```java { .api }
115
/**
116
 * Indicates which methods have been called on the object
117
 */
118
@Documented
119
@Retention(RetentionPolicy.RUNTIME)
120
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
121
@SubtypeOf(CalledMethodsBottom.class)
122
public @interface CalledMethods {
123
    String[] value();
124
}
125

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

130
/**
131
 * Predicate over called methods (for complex conditions)
132
 */
133
@Documented
134
@Retention(RetentionPolicy.RUNTIME)
135
@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
136
public @interface CalledMethodsPredicate {
137
    String value();
138
}
139
```
140

141
**Usage Examples:**
142

143
```java
144
import org.checkerframework.checker.calledmethods.qual.*;
145

146
public class DatabaseConnection {
147
    private boolean connected = false;
148
    private boolean authenticated = false;
149
    
150
    public void connect() {
151
        this.connected = true;
152
    }
153
    
154
    public void authenticate(String username, String password) {
155
        if (!connected) {
156
            throw new IllegalStateException("Must connect first");
157
        }
158
        this.authenticated = true;
159
    }
160
    
161
    public void executeQuery(String query) {
162
        if (!connected || !authenticated) {
163
            throw new IllegalStateException("Must connect and authenticate first");
164
        }
165
        System.out.println("Executing: " + query);
166
    }
167
    
168
    public void disconnect() {
169
        this.connected = false;
170
        this.authenticated = false;
171
    }
172
}
173

174
public class CalledMethodsExample {
175
    public void safeDatabase() {
176
        DatabaseConnection db = new DatabaseConnection();
177
        
178
        // Track method calls
179
        db.connect();
180
        @CalledMethods("connect") DatabaseConnection connectedDb = db;
181
        
182
        db.authenticate("user", "pass");
183
        @CalledMethods({"connect", "authenticate"}) DatabaseConnection authDb = db;
184
        
185
        // Safe to execute query after both methods called
186
        authDb.executeQuery("SELECT * FROM users");
187
        
188
        db.disconnect();
189
    }
190
    
191
    // Method that requires specific methods to have been called
192
    public void processConnectedDatabase(@CalledMethods("connect") DatabaseConnection db) {
193
        // Can safely assume connect() has been called
194
        db.authenticate("admin", "secret");
195
        db.executeQuery("SELECT * FROM admin_table");
196
    }
197
}
198
```
199

200
### Ownership Annotations
201

202
Annotations that track resource ownership and transfer.
203

204
```java { .api }
205
/**
206
 * Parameter takes ownership of the resource
207
 */
208
@Documented
209
@Retention(RetentionPolicy.RUNTIME)
210
@Target(ElementType.PARAMETER)
211
public @interface Owning {}
212

213
/**
214
 * Parameter does not take ownership of the resource
215
 */
216
@Documented
217
@Retention(RetentionPolicy.RUNTIME)
218
@Target(ElementType.PARAMETER)
219
public @interface NotOwning {}
220
```
221

222
**Usage Examples:**
223

224
```java
225
import org.checkerframework.checker.mustcall.qual.*;
226
import java.io.Closeable;
227

228
public class OwnershipExample {
229
    // Method takes ownership and is responsible for closing
230
    public void processAndClose(@Owning @MustCall("close") Closeable resource) {
231
        try {
232
            // Process the resource
233
            System.out.println("Processing resource");
234
        } finally {
235
            try {
236
                resource.close(); // Owner must close
237
            } catch (Exception e) {
238
                // Handle close error
239
            }
240
        }
241
    }
242
    
243
    // Method uses resource but doesn't take ownership
244
    public void processOnly(@NotOwning @MustCall("close") Closeable resource) {
245
        // Use the resource but don't close it
246
        System.out.println("Using resource");
247
        // Caller is still responsible for closing
248
    }
249
    
250
    public void example() throws Exception {
251
        @MustCall("close") FileInputStream file = new FileInputStream("data.txt");
252
        
253
        // Transfer ownership - file will be closed by processAndClose
254
        processAndClose(file);
255
        // Don't close file here - ownership was transferred
256
        
257
        @MustCall("close") FileInputStream file2 = new FileInputStream("data2.txt");
258
        try {
259
            // Use without transferring ownership
260
            processOnly(file2);
261
            // Still responsible for closing since ownership not transferred
262
        } finally {
263
            file2.close();
264
        }
265
    }
266
}
267
```
268

269
### Side Effect Tracking
270

271
Annotations for tracking side effects that create or modify must-call obligations.
272

273
```java { .api }
274
/**
275
 * Method creates must-call obligations for specified expressions
276
 */
277
@Target(ElementType.METHOD)
278
@Retention(RetentionPolicy.RUNTIME)
279
@InheritedAnnotation
280
public @interface CreatesMustCallFor {
281
    String[] value();
282
}
283
```
284

285
**Usage Examples:**
286

287
```java
288
import org.checkerframework.checker.mustcall.qual.*;
289
import java.io.*;
290

291
public class ConnectionPool {
292
    private List<@MustCall("close") Connection> activeConnections = new ArrayList<>();
293
    
294
    @CreatesMustCallFor("this")
295
    public Connection borrowConnection() {
296
        @MustCall("close") Connection conn = new Connection();
297
        activeConnections.add(conn);
298
        return conn; // Creates must-call obligation for the pool
299
    }
300
    
301
    public void returnConnection(@MustCall("close") Connection conn) {
302
        activeConnections.remove(conn);
303
        // Connection is returned to pool, not closed yet
304
    }
305
    
306
    @MustCall("closeAll")
307
    public void closeAll() {
308
        for (@MustCall("close") Connection conn : activeConnections) {
309
            try {
310
                conn.close();
311
            } catch (Exception e) {
312
                // Log error
313
            }
314
        }
315
        activeConnections.clear();
316
    }
317
}
318

319
@MustCall("close")
320
class Connection {
321
    private boolean closed = false;
322
    
323
    public void execute(String command) {
324
        if (closed) throw new IllegalStateException("Connection closed");
325
        System.out.println("Executing: " + command);
326
    }
327
    
328
    public void close() {
329
        this.closed = true;
330
    }
331
}
332

333
public class SideEffectExample {
334
    public void useConnectionPool() {
335
        @MustCall("closeAll") ConnectionPool pool = new ConnectionPool();
336
        
337
        // borrowConnection creates must-call obligation for pool
338
        @MustCall("close") Connection conn1 = pool.borrowConnection();
339
        @MustCall("close") Connection conn2 = pool.borrowConnection();
340
        
341
        try {
342
            conn1.execute("SELECT * FROM users");
343
            conn2.execute("UPDATE settings SET value = 'new' WHERE key = 'config'");
344
        } finally {
345
            // Return connections to pool
346
            pool.returnConnection(conn1);
347
            pool.returnConnection(conn2);
348
            
349
            // Pool must close all connections
350
            pool.closeAll(); // Required due to @CreatesMustCallFor
351
        }
352
    }
353
}
354
```
355

356
### Method Contract Annotations
357

358
Annotations for expressing resource-related method contracts.
359

360
```java { .api }
361
/**
362
 * Method postcondition: ensures specified methods are called on expressions
363
 */
364
@Target(ElementType.METHOD)
365
@Retention(RetentionPolicy.RUNTIME)
366
@InheritedAnnotation
367
public @interface EnsuresCalledMethods {
368
    String[] value();
369
    String[] methods();
370
}
371

372
/**
373
 * Conditional method postcondition for called methods
374
 */
375
@Target(ElementType.METHOD)
376
@Retention(RetentionPolicy.RUNTIME)
377
@InheritedAnnotation
378
public @interface EnsuresCalledMethodsIf {
379
    String[] expression();
380
    String[] methods();
381
    boolean result();
382
}
383

384
/**
385
 * Exception postcondition: ensures methods are called when exception thrown
386
 */
387
@Target(ElementType.METHOD)
388
@Retention(RetentionPolicy.RUNTIME)
389
@InheritedAnnotation
390
public @interface EnsuresCalledMethodsOnException {
391
    String[] value();
392
    String[] methods();
393
    Class<? extends Throwable>[] exception() default {Throwable.class};
394
}
395

396
/**
397
 * Varargs version of EnsuresCalledMethods
398
 */
399
@Target(ElementType.METHOD)
400
@Retention(RetentionPolicy.RUNTIME)
401
@InheritedAnnotation
402
public @interface EnsuresCalledMethodsVarargs {
403
    String[] value();
404
    String[] methods();
405
}
406

407
/**
408
 * Method precondition: requires specified methods to have been called
409
 */
410
@Target(ElementType.METHOD)
411
@Retention(RetentionPolicy.RUNTIME)
412
@InheritedAnnotation
413
public @interface RequiresCalledMethods {
414
    String[] value();
415
    String[] methods();
416
}
417
```
418

419
**Usage Examples:**
420

421
```java
422
import org.checkerframework.checker.calledmethods.qual.*;
423

424
public class ContractResourceExample {
425
    private DatabaseConnection connection;
426
    
427
    @EnsuresCalledMethods(value = "connection", methods = {"connect"})
428
    public void initialize() {
429
        connection = new DatabaseConnection();
430
        connection.connect(); // Postcondition ensures connect() is called
431
    }
432
    
433
    @EnsuresCalledMethodsIf(expression = "connection", methods = {"connect", "authenticate"}, result = true)
434
    public boolean isReady() {
435
        return connection != null && 
436
               connection.isConnected() && 
437
               connection.isAuthenticated();
438
    }
439
    
440
    @RequiresCalledMethods(value = "connection", methods = {"connect"})
441
    public void authenticate(String user, String password) {
442
        // Precondition: connect() must have been called
443
        connection.authenticate(user, password);
444
    }
445
    
446
    @EnsuresCalledMethodsOnException(value = "connection", methods = {"disconnect"}, exception = {SQLException.class})
447
    public void riskyOperation() throws SQLException {
448
        try {
449
            connection.executeQuery("RISKY OPERATION");
450
        } catch (SQLException e) {
451
            connection.disconnect(); // Cleanup on exception
452
            throw e;
453
        }
454
    }
455
    
456
    public void safeUsage() throws SQLException {
457
        initialize(); // Ensures connect() is called
458
        authenticate("user", "pass"); // Safe - connect() was called
459
        
460
        if (isReady()) {
461
            // Safe - conditional postcondition ensures both methods called
462
            connection.executeQuery("SELECT * FROM data");
463
        }
464
        
465
        try {
466
            riskyOperation();
467
        } catch (SQLException e) {
468
            // Exception postcondition ensures disconnect() was called
469
            System.out.println("Operation failed, connection cleaned up");
470
        }
471
    }
472
}
473
```