0
# Method Contracts and Side Effects
1

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

4
## Capabilities
5

6
### Purity Annotations
7

8
Annotations that specify method purity and side effect properties.
9

10
```java { .api }
11
/**
12
 * Method has no side effects and returns the same result for same inputs
13
 */
14
@Documented
15
@Retention(RetentionPolicy.RUNTIME)
16
@Target(ElementType.METHOD)
17
public @interface Pure {}
18

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

27
/**
28
 * Method returns the same result for same inputs but may have side effects
29
 */
30
@Documented
31
@Retention(RetentionPolicy.RUNTIME)
32
@Target(ElementType.METHOD)
33
public @interface Deterministic {}
34

35
/**
36
 * Method terminates execution (throws exception or calls System.exit)
37
 */
38
@Documented
39
@Retention(RetentionPolicy.RUNTIME)
40
@Target(ElementType.METHOD)
41
public @interface TerminatesExecution {}
42

43
/**
44
 * Indicates method is unqualified for purity analysis
45
 */
46
@Documented
47
@Retention(RetentionPolicy.RUNTIME)
48
@Target(ElementType.METHOD)
49
public @interface PurityUnqualified {}
50
```
51

52
**Usage Examples:**
53

54
```java
55
import org.checkerframework.dataflow.qual.*;
56

57
public class PurityExample {
58
    private int counter = 0;
59
    
60
    // Pure method - no side effects, same result for same inputs
61
    @Pure
62
    public int add(int a, int b) {
63
        return a + b; // Always returns same result for same inputs
64
    }
65
    
66
    // Side-effect free but not deterministic
67
    @SideEffectFree
68
    public long getCurrentTime() {
69
        return System.currentTimeMillis(); // No side effects, but result varies
70
    }
71
    
72
    // Deterministic but has side effects
73
    @Deterministic
74
    public int getAndIncrement() {
75
        return counter++; // Side effect: modifies counter, but deterministic sequence
76
    }
77
    
78
    // Method that always throws exception
79
    @TerminatesExecution
80
    public void fail(String message) {
81
        throw new RuntimeException(message); // Never returns normally
82
    }
83
    
84
    // Complex method that can't be classified for purity
85
    @PurityUnqualified
86
    public void complexOperation() {
87
        // Complex logic that doesn't fit purity categories
88
        if (Math.random() > 0.5) {
89
            counter++;
90
        }
91
        System.out.println("Operation complete");
92
    }
93
    
94
    public void example() {
95
        // Pure methods can be called multiple times safely
96
        int result1 = add(5, 3); // 8
97
        int result2 = add(5, 3); // Always 8
98
        assert result1 == result2; // Always true
99
        
100
        // Side-effect free methods don't modify state
101
        long time1 = getCurrentTime();
102
        long time2 = getCurrentTime(); // May be different
103
        
104
        // Deterministic methods have predictable sequences
105
        int seq1 = getAndIncrement(); // 0
106
        int seq2 = getAndIncrement(); // 1
107
        int seq3 = getAndIncrement(); // 2
108
        
109
        // Method that terminates execution
110
        try {
111
            fail("Something went wrong");
112
        } catch (RuntimeException e) {
113
            System.out.println("Caught expected exception");
114
        }
115
    }
116
}
117
```
118

119
### Nullness Contract Annotations
120

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

123
```java { .api }
124
/**
125
 * Method postcondition: ensures expressions are non-null after execution
126
 */
127
@Target(ElementType.METHOD)
128
@Retention(RetentionPolicy.RUNTIME)
129
@InheritedAnnotation
130
public @interface EnsuresNonNull {
131
    String[] value();
132
}
133

134
/**
135
 * Conditional nullness postcondition
136
 */
137
@Target(ElementType.METHOD)
138
@Retention(RetentionPolicy.RUNTIME)
139
@InheritedAnnotation
140
public @interface EnsuresNonNullIf {
141
    String[] expression();
142
    boolean result();
143
}
144

145
/**
146
 * Method precondition: requires expressions to be non-null
147
 */
148
@Target(ElementType.METHOD)
149
@Retention(RetentionPolicy.RUNTIME)
150
@InheritedAnnotation
151
public @interface RequiresNonNull {
152
    String[] value();
153
}
154
```
155

156
**Usage Examples:**
157

158
```java
159
import org.checkerframework.checker.nullness.qual.*;
160

161
public class NullnessContractExample {
162
    private String data;
163
    private String backup;
164
    
165
    @EnsuresNonNull("data")
166
    public void initializeData(String value) {
167
        this.data = value; // Postcondition: data is non-null
168
    }
169
    
170
    @EnsuresNonNullIf(expression = {"data", "backup"}, result = true)
171
    public boolean isFullyInitialized() {
172
        return data != null && backup != null;
173
    }
174
    
175
    @RequiresNonNull("data")
176
    public void processData() {
177
        // Precondition: data must be non-null
178
        System.out.println("Processing: " + data.length() + " characters");
179
    }
180
    
181
    @EnsuresNonNull("backup")
182
    public void createBackup() {
183
        this.backup = this.data != null ? this.data + "_backup" : "empty_backup";
184
    }
185
    
186
    public void safeWorkflow() {
187
        initializeData("Hello World"); // Ensures data is non-null
188
        processData(); // Safe - postcondition guarantees data is non-null
189
        
190
        createBackup(); // Ensures backup is non-null
191
        
192
        if (isFullyInitialized()) {
193
            // Safe - conditional postcondition guarantees both are non-null
194
            System.out.println("Data: " + data + ", Backup: " + backup);
195
        }
196
    }
197
}
198
```
199

200
### Lock Contract Annotations
201

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

204
```java { .api }
205
/**
206
 * Method requires specified locks to be held when called
207
 */
208
@Target(ElementType.METHOD)
209
@Retention(RetentionPolicy.RUNTIME)
210
@InheritedAnnotation
211
public @interface Holding {
212
    String[] value();
213
}
214

215
/**
216
 * Method postcondition: ensures locks are held after execution
217
 */
218
@Target(ElementType.METHOD)
219
@Retention(RetentionPolicy.RUNTIME)
220
@InheritedAnnotation
221
public @interface EnsuresLockHeld {
222
    String[] value();
223
}
224

225
/**
226
 * Conditional lock postcondition
227
 */
228
@Target(ElementType.METHOD)
229
@Retention(RetentionPolicy.RUNTIME)
230
@InheritedAnnotation
231
public @interface EnsuresLockHeldIf {
232
    String[] expression();
233
    boolean result();
234
}
235
```
236

237
**Usage Examples:**
238

239
```java
240
import org.checkerframework.checker.lock.qual.*;
241

242
public class LockContractExample {
243
    private final Object dataLock = new Object();
244
    private final Object stateLock = new Object();
245
    private String sharedData;
246
    private boolean initialized = false;
247
    
248
    @EnsuresLockHeld("dataLock")
249
    public void acquireDataLock() {
250
        synchronized (dataLock) {
251
            // Lock acquired - postcondition ensures it's held
252
        }
253
    }
254
    
255
    @Holding("dataLock")
256
    public void updateData(String newData) {
257
        // Precondition: dataLock must be held
258
        this.sharedData = newData;
259
    }
260
    
261
    @EnsuresLockHeldIf(expression = "stateLock", result = true)
262
    public boolean tryInitialize() {
263
        synchronized (stateLock) {
264
            if (!initialized) {
265
                initialized = true;
266
                return true; // Lock is held when returning true
267
            }
268
        }
269
        return false; // Lock not held when returning false
270
    }
271
    
272
    public void concurrentWorkflow() {
273
        synchronized (dataLock) {
274
            updateData("New value"); // Safe - lock is held
275
        }
276
        
277
        if (tryInitialize()) {
278
            // Safe - conditional postcondition ensures stateLock is held
279
            // Can safely access state protected by stateLock
280
            System.out.println("Initialization successful");
281
        }
282
    }
283
}
284
```
285

286
### Index and Bounds Contract Annotations
287

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

290
```java { .api }
291
/**
292
 * Method postcondition: ensures expression is less than length of arrays
293
 */
294
@Target(ElementType.METHOD)
295
@Retention(RetentionPolicy.RUNTIME)
296
@InheritedAnnotation
297
public @interface EnsuresLTLengthOf {
298
    String[] value();
299
    String[] targetValue();
300
}
301

302
/**
303
 * Conditional bounds postcondition
304
 */
305
@Target(ElementType.METHOD)
306
@Retention(RetentionPolicy.RUNTIME)
307
@InheritedAnnotation
308
public @interface EnsuresLTLengthOfIf {
309
    String[] expression();
310
    boolean result();
311
    String[] targetValue();
312
}
313
```
314

315
**Usage Examples:**
316

317
```java
318
import org.checkerframework.checker.index.qual.*;
319

320
public class BoundsContractExample {
321
    private int[] data = new int[100];
322
    private int currentIndex = 0;
323
    
324
    @EnsuresLTLengthOf(value = "currentIndex", targetValue = "data")
325
    public void resetIndex() {
326
        currentIndex = 0; // Postcondition: currentIndex < data.length
327
    }
328
    
329
    @EnsuresLTLengthOfIf(expression = "currentIndex", result = true, targetValue = "data")
330
    public boolean hasNext() {
331
        return currentIndex < data.length;
332
    }
333
    
334
    public void safeBoundsIteration() {
335
        resetIndex(); // Ensures currentIndex < data.length
336
        
337
        while (hasNext()) {
338
            // Safe - conditional postcondition ensures currentIndex < data.length
339
            System.out.println(data[currentIndex]);
340
            currentIndex++;
341
        }
342
    }
343
}
344
```
345

346
### Generic Contract Framework
347

348
Framework for creating custom method contracts.
349

350
```java { .api }
351
/**
352
 * Generic method postcondition
353
 */
354
@Target(ElementType.METHOD)
355
@Retention(RetentionPolicy.RUNTIME)
356
@InheritedAnnotation
357
public @interface EnsuresQualifier {
358
    String[] expression();
359
    Class<? extends Annotation> qualifier();
360
}
361

362
/**
363
 * Generic conditional method postcondition
364
 */
365
@Target(ElementType.METHOD)
366
@Retention(RetentionPolicy.RUNTIME)
367
@InheritedAnnotation
368
public @interface EnsuresQualifierIf {
369
    String[] expression();
370
    Class<? extends Annotation> qualifier();
371
    boolean result();
372
}
373

374
/**
375
 * Generic method precondition
376
 */
377
@Target(ElementType.METHOD)
378
@Retention(RetentionPolicy.RUNTIME)
379
@InheritedAnnotation
380
public @interface RequiresQualifier {
381
    String[] expression();
382
    Class<? extends Annotation> qualifier();
383
}
384
```
385

386
**Usage Examples:**
387

388
```java
389
import org.checkerframework.framework.qual.*;
390

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

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

401
public class GenericContractExample {
402
    @EnsuresQualifier(expression = "#1", qualifier = Validated.class)
403
    public String validate(String input) {
404
        if (input == null || input.trim().isEmpty()) {
405
            throw new IllegalArgumentException("Invalid input");
406
        }
407
        return input; // Postcondition: result is @Validated
408
    }
409
    
410
    @RequiresQualifier(expression = "#1", qualifier = Validated.class)
411
    @EnsuresQualifier(expression = "#1", qualifier = Sanitized.class)
412
    public String sanitize(@Validated String input) {
413
        // Precondition: input must be @Validated
414
        // Remove potentially dangerous characters
415
        String sanitized = input.replaceAll("[<>\"'&]", "");
416
        return sanitized; // Postcondition: result is @Sanitized
417
    }
418
    
419
    @EnsuresQualifierIf(expression = "#1", qualifier = Validated.class, result = true)
420
    public boolean isValid(String input) {
421
        return input != null && !input.trim().isEmpty();
422
    }
423
    
424
    public void processingPipeline(String userInput) {
425
        if (isValid(userInput)) {
426
            // Conditional postcondition: userInput is @Validated
427
            @Validated String validInput = (@Validated String) userInput;
428
            
429
            @Sanitized String safeInput = sanitize(validInput); // Safe - precondition met
430
            
431
            // Use sanitized input safely
432
            System.out.println("Processing: " + safeInput);
433
        } else {
434
            System.out.println("Invalid input provided");
435
        }
436
    }
437
}
438
```
439

440
### Advanced Contract Patterns
441

442
Complex contract combinations and patterns.
443

444
**Builder Pattern with Contracts:**
445

446
```java
447
import org.checkerframework.checker.calledmethods.qual.*;
448
import org.checkerframework.dataflow.qual.*;
449

450
public class ContractBuilderExample {
451
    @MustCall("build")
452
    public static class ConfigBuilder {
453
        private String host;
454
        private int port = 80;
455
        private boolean secure = false;
456
        
457
        @EnsuresCalledMethods(value = "this", methods = {"setHost"})
458
        public ConfigBuilder host(String host) {
459
            this.host = host;
460
            return this;
461
        }
462
        
463
        public ConfigBuilder port(int port) {
464
            this.port = port;
465
            return this;
466
        }
467
        
468
        public ConfigBuilder secure(boolean secure) {
469
            this.secure = secure;
470
            return this;
471
        }
472
        
473
        @RequiresCalledMethods(value = "this", methods = {"setHost"})
474
        @Pure
475
        public Config build() {
476
            return new Config(host, port, secure);
477
        }
478
    }
479
    
480
    public static class Config {
481
        private final String host;
482
        private final int port;
483
        private final boolean secure;
484
        
485
        Config(String host, int port, boolean secure) {
486
            this.host = host;
487
            this.port = port;
488
            this.secure = secure;
489
        }
490
        
491
        @Pure
492
        public String getHost() { return host; }
493
        
494
        @Pure
495
        public int getPort() { return port; }
496
        
497
        @Pure
498
        public boolean isSecure() { return secure; }
499
    }
500
    
501
    public void builderExample() {
502
        // Correct usage - host is required
503
        Config config1 = new ConfigBuilder()
504
            .host("example.com")  // Required method call
505
            .port(443)
506
            .secure(true)
507
            .build(); // Safe - host was called
508
        
509
        // This would cause a type error:
510
        // Config config2 = new ConfigBuilder()
511
        //     .port(80)
512
        //     .build(); // Error - host() must be called first
513
    }
514
}
515
```